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