DEFINITION lift_gen_lref_ge()
TYPE =
       ∀h:nat
         .∀d:nat
           .∀n:nat
             .le d n
               →∀t:T
                    .(eq T (TLRef (plus n h)) (lift h d t))→(eq T t (TLRef n))
BODY =
Show proof