DEFINITION O_S()
TYPE =
       ∀n:nat.(not (eq nat O (S n)))
BODY =
Show proof