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