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