DEFINITION eq_add_S()
TYPE =
       ∀n:nat.∀m:nat.(eq nat (S n) (S m))→(eq nat n m)
BODY =
        assume n: nat
        assume m: nat
        suppose H: eq nat (S n) (S m)
          by (f_equal . . . . . H)
          we proved eq nat (pred (S n)) (pred (S m))
          that is equivalent to eq nat n m
       we proved ∀n:nat.∀m:nat.(eq nat (S n) (S m))→(eq nat n m)