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