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