DEFINITION s_inc()
TYPE =
       ∀k:K.∀i:nat.(le i (s k i))
BODY =
       assume k: K
          we proceed by induction on k to prove ∀i:nat.(le i (s k i))
             case Bind : b:B ⇒
                the thesis becomes ∀i:nat.(le i (s (Bind b) i))
                   assume i: nat
                      by (le_n .)
                      we proved le (s (Bind b) i) (s (Bind b) i)
                      that is equivalent to le (S i) (s (Bind b) i)
                      by (le_S . . previous)
                      we proved le (S i) (S (s (Bind b) i))
                      by (le_S_n . . previous)
                      we proved le i (s (Bind b) i)
∀i:nat.(le i (s (Bind b) i))
             case Flat : f:F ⇒
                the thesis becomes ∀i:nat.(le (s (Flat f) i) (s (Flat f) i))
                   assume i: nat
                      by (le_n .)
                      we proved le (s (Flat f) i) (s (Flat f) i)
                      that is equivalent to le i (s (Flat f) i)
∀i:nat.(le (s (Flat f) i) (s (Flat f) i))
          we proved ∀i:nat.(le i (s k i))
       we proved ∀k:K.∀i:nat.(le i (s k i))