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