DEFINITION lift_gen_lref()
TYPE =
       ∀t:T
         .∀d:nat
           .∀h:nat
             .∀i:nat
               .eq T (TLRef i) (lift h d t)
                 →(or
                      land (lt i d) (eq T t (TLRef i))
                      land (le (plus d h) i) (eq T t (TLRef (minus i h))))
BODY =
Show proof