DEFINITION pred_Sn()
TYPE =
       ∀m:nat.(eq nat m (pred (S m)))
BODY =
       assume m: nat
          by (refl_equal . .)
          we proved eq nat (pred (S m)) (pred (S m))
          that is equivalent to eq nat m (pred (S m))
       we proved ∀m:nat.(eq nat m (pred (S m)))