DEFINITION lift_lref_gt()
TYPE =
       ∀d:nat
         .∀n:nat
           .lt d n
             →eq T (lift (S O) d (TLRef (pred n))) (TLRef n)
BODY =
Show proof