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