DEFINITION subst_lref_eq()
TYPE =
       ∀v:T.∀i:nat.(eq T (subst i v (TLRef i)) (lift i O v))
BODY =
Show proof