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