DEFINITION s_plus_sym()
TYPE =
       ∀k:K.∀i:nat.∀j:nat.(eq nat (s k (plus i j)) (plus i (s k j)))
BODY =
       assume k: K
          we proceed by induction on k to prove ∀i:nat.∀j:nat.(eq nat (s k (plus i j)) (plus i (s k j)))
             case Bind : :B ⇒
                the thesis becomes ∀i:nat.∀j:nat.(eq nat (S (plus i j)) (plus i (S j)))
                    assume i: nat
                    assume j: nat
                      (h1) 
                         by (refl_equal . .)
eq nat (plus i (S j)) (plus i (S j))
                      end of h1
                      (h2) 
                         by (plus_n_Sm . .)
eq nat (S (plus i j)) (plus i (S j))
                      end of h2
                      by (eq_ind_r . . . h1 . h2)
                      we proved eq nat (S (plus i j)) (plus i (S j))
                      that is equivalent to eq nat (s (Bind __3) (plus i j)) (plus i (s (Bind __3) j))
∀i:nat.∀j:nat.(eq nat (S (plus i j)) (plus i (S j)))
             case Flat : f:F ⇒
                the thesis becomes 
                ∀i:nat
                  .∀j:nat.(eq nat (plus i (s (Flat f) j)) (plus i (s (Flat f) j)))
                    assume i: nat
                    assume j: nat
                      by (refl_equal . .)
                      we proved eq nat (plus i (s (Flat f) j)) (plus i (s (Flat f) j))
                      that is equivalent to eq nat (s (Flat f) (plus i j)) (plus i (s (Flat f) j))

                      ∀i:nat
                        .∀j:nat.(eq nat (plus i (s (Flat f) j)) (plus i (s (Flat f) j)))
          we proved ∀i:nat.∀j:nat.(eq nat (s k (plus i j)) (plus i (s k j)))
       we proved ∀k:K.∀i:nat.∀j:nat.(eq nat (s k (plus i j)) (plus i (s k j)))