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 =
Show proof