DEFINITION lift_lref_lt()
TYPE =
       ∀n:nat
         .∀h:nat.∀d:nat.(lt n d)→(eq T (lift h d (TLRef n)) (TLRef n))
BODY =
        assume n: nat
        assume h: nat
        assume d: nat
        suppose H: lt n d
          by (lt_blt . . H)
          we proved eq bool (blt n d) true
          by (sym_eq . . . previous)
          we proved eq bool true (blt n d)
          we proceed by induction on the previous result to prove 
             eq
               T
               TLRef <λb1:bool.nat> CASE blt n d OF true⇒n | false⇒plus n h
               TLRef n
             case refl_equal : ⇒
                the thesis becomes 
                eq
                  T
                  TLRef <λb1:bool.nat> CASE true OF true⇒n | false⇒plus n h
                  TLRef n
                   by (refl_equal . .)
                   we proved eq T (TLRef n) (TLRef n)

                      eq
                        T
                        TLRef <λb1:bool.nat> CASE true OF true⇒n | false⇒plus n h
                        TLRef n
          we proved 
             eq
               T
               TLRef <λb1:bool.nat> CASE blt n d OF true⇒n | false⇒plus n h
               TLRef n
          that is equivalent to eq T (lift h d (TLRef n)) (TLRef n)
       we proved 
          ∀n:nat
            .∀h:nat.∀d:nat.(lt n d)→(eq T (lift h d (TLRef n)) (TLRef n))