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