DEFINITION tweight_lt()
TYPE =
       ∀t:T.(lt O (tweight t))
BODY =
       assume t: T
          we proceed by induction on t to prove lt O (tweight t)
             case TSort : :nat ⇒
                the thesis becomes lt O (tweight (TSort __1))
                   by (le_n .)
                   we proved le (S O) (S O)
lt O (tweight (TSort __1))
             case TLRef : :nat ⇒
                the thesis becomes lt O (tweight (TLRef __1))
                   by (le_n .)
                   we proved le (S O) (S O)
lt O (tweight (TLRef __1))
             case THead : :K t0:T t1:T ⇒
                the thesis becomes lt O (tweight (THead __5 t0 t1))
                (H) by induction hypothesis we know lt O (tweight t0)
                () by induction hypothesis we know lt O (tweight t1)
                   consider H
                   we proved lt O (tweight t0)
                   that is equivalent to le (S O) (tweight t0)
                   by (le_plus_trans . . . previous)
                   we proved le (S O) (plus (tweight t0) (tweight t1))
                   by (le_S . . previous)
                   we proved le (S O) (S (plus (tweight t0) (tweight t1)))
lt O (tweight (THead __5 t0 t1))
          we proved lt O (tweight t)
       we proved ∀t:T.(lt O (tweight t))