DEFINITION s_le()
TYPE =
       ∀k:K.∀i:nat.∀j:nat.(le i j)→(le (s k i) (s k j))
BODY =
       assume k: K
          we proceed by induction on k to prove ∀i:nat.∀j:nat.(le i j)→(le (s k i) (s k j))
             case Bind : :B ⇒
                the thesis becomes ∀i:nat.∀j:nat.∀H:(le i j).(le (S i) (S j))
                    assume i: nat
                    assume j: nat
                    suppose H: le i j
                      by (le_n_S . . H)
                      we proved le (S i) (S j)
                      that is equivalent to le (s (Bind __4) i) (s (Bind __4) j)
∀i:nat.∀j:nat.∀H:(le i j).(le (S i) (S j))
             case Flat : :F ⇒
                the thesis becomes ∀i:nat.∀j:nat.∀H:(le i j).(le i j)
                    assume i: nat
                    assume j: nat
                    suppose H: le i j
                      consider H
                      we proved le i j
                      that is equivalent to le (s (Flat __4) i) (s (Flat __4) j)
∀i:nat.∀j:nat.∀H:(le i j).(le i j)
          we proved ∀i:nat.∀j:nat.(le i j)→(le (s k i) (s k j))
       we proved ∀k:K.∀i:nat.∀j:nat.(le i j)→(le (s k i) (s k j))