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