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