DEFINITION r_plus()
TYPE =
       ∀k:K.∀i:nat.∀j:nat.(eq nat (r k (plus i j)) (plus (r k i) 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 (r k i) j))
             case Bind : b:B ⇒
                the thesis becomes 
                ∀i:nat
                  .∀j:nat.(eq nat (plus (r (Bind b) i) j) (plus (r (Bind b) i) j))
                    assume i: nat
                    assume j: nat
                      by (refl_equal . .)
                      we proved eq nat (plus (r (Bind b) i) j) (plus (r (Bind b) i) j)
                      that is equivalent to eq nat (r (Bind b) (plus i j)) (plus (r (Bind b) i) j)

                      ∀i:nat
                        .∀j:nat.(eq nat (plus (r (Bind b) i) j) (plus (r (Bind b) i) j))
             case Flat : f:F ⇒
                the thesis becomes 
                ∀i:nat
                  .∀j:nat.(eq nat (plus (r (Flat f) i) j) (plus (r (Flat f) i) j))
                    assume i: nat
                    assume j: nat
                      by (refl_equal . .)
                      we proved eq nat (plus (r (Flat f) i) j) (plus (r (Flat f) i) j)
                      that is equivalent to eq nat (r (Flat f) (plus i j)) (plus (r (Flat f) i) j)

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