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