DEFINITION pred_Sn()
TYPE =
       ∀m:nat.(eq nat m (pred (S m)))
BODY =
Show proof