DEFINITION lift_lref_ge()
TYPE =
       ∀n:nat
         .∀h:nat
           .∀d:nat
             .(le d n)→(eq T (lift h d (TLRef n)) (TLRef (plus n h)))
BODY =
        assume n: nat
        assume h: nat
        assume d: nat
        suppose H: le d n
          by (le_bge . . H)
          we proved eq bool (blt n d) false
          by (sym_eq . . . previous)
          we proved eq bool false (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 (plus n h)
             case refl_equal : ⇒
                the thesis becomes 
                eq
                  T
                  TLRef <λb1:bool.nat> CASE false OF true⇒n | false⇒plus n h
                  TLRef (plus n h)
                   by (refl_equal . .)
                   we proved eq T (TLRef (plus n h)) (TLRef (plus n h))

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