DEFINITION simpl_plus_r()
TYPE =
       ∀n:nat.∀m:nat.∀p:nat.(eq nat (plus m n) (plus p n))→(eq nat m p)
BODY =
Show proof