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 =
        assume n: nat
        assume h: nat
        assume k: nat
          (h1) 
             (h1) 
                by (refl_equal . .)
eq nat (plus (plus n k) h) (plus (plus n k) h)
             end of h1
             (h2) 
                by (plus_assoc_l . . .)
eq nat (plus n (plus k h)) (plus (plus n k) h)
             end of h2
             by (eq_ind_r . . . h1 . h2)
eq nat (plus (plus n k) h) (plus n (plus k h))
          end of h1
          (h2) 
             by (plus_permute_2_in_3 . . .)
eq nat (plus (plus n h) k) (plus (plus n k) h)
          end of h2
          by (eq_ind_r . . . h1 . h2)
          we proved eq nat (plus (plus n h) k) (plus n (plus k h))
       we proved ∀n:nat.∀h:nat.∀k:nat.(eq nat (plus (plus n h) k) (plus n (plus k h)))