DEFINITION not_eq_S()
TYPE =
       ∀n:nat.∀m:nat.(not (eq nat n m))→(not (eq nat (S n) (S m)))
BODY =
Show proof