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