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