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