DEFINITION subst_lref_gt()
TYPE =
       ∀v:T
         .∀d:nat
           .∀i:nat
             .(lt d i)→(eq T (subst d v (TLRef i)) (TLRef (pred i)))
BODY =
Show proof