DEFINITION plus_permute_2_in_3_assoc()
TYPE =
       ∀n:nat.∀h:nat.∀k:nat.(eq nat (plus (plus n h) k) (plus n (plus k h)))
BODY =
Show proof