DEFINITION subst0_gen_lref()
TYPE =
       ∀v:T
         .∀x:T
           .∀i:nat
             .∀n:nat
               .subst0 i v (TLRef n) x
                 →land (eq nat n i) (eq T x (lift (S n) O v))
BODY =
Show proof