DEFINITION plus_permute_2_in_3()
TYPE =
       ∀x:nat.∀y:nat.∀z:nat.(eq nat (plus (plus x y) z) (plus (plus x z) y))
BODY =
Show proof