DEFINITION lift_tlt_dx()
TYPE =
       ∀k:K.∀u:T.∀t:T.∀h:nat.∀d:nat.(tlt t (THead k u (lift h d t)))
BODY =
        assume k: K
        assume u: T
        assume t: T
        assume h: nat
        assume d: nat
          by (lift_weight . . .)
          we proved eq nat (weight (lift h d t)) (weight t)
          we proceed by induction on the previous result to prove lt (weight t) (weight (THead k u (lift h d t)))
             case refl_equal : ⇒
                the thesis becomes lt (weight (lift h d t)) (weight (THead k u (lift h d t)))
                   by (tlt_head_dx . . .)
                   we proved tlt (lift h d t) (THead k u (lift h d t))
lt (weight (lift h d t)) (weight (THead k u (lift h d t)))
          we proved lt (weight t) (weight (THead k u (lift h d t)))
          that is equivalent to tlt t (THead k u (lift h d t))
       we proved ∀k:K.∀u:T.∀t:T.∀h:nat.∀d:nat.(tlt t (THead k u (lift h d t)))