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 =
        assume v: T
        assume x: T
        assume i: nat
        assume n: nat
        suppose H: subst1 i v (TLRef n) x
          we proceed by induction on H to prove 
             or
               eq T x (TLRef n)
               land (eq nat n i) (eq T x (lift (S n) O v))
             case subst1_refl : ⇒
                the thesis becomes 
                or
                  eq T (TLRef n) (TLRef n)
                  land (eq nat n i) (eq T (TLRef n) (lift (S n) O v))
                   by (refl_equal . .)
                   we proved eq T (TLRef n) (TLRef n)
                   by (or_introl . . previous)

                      or
                        eq T (TLRef n) (TLRef n)
                        land (eq nat n i) (eq T (TLRef n) (lift (S n) O v))
             case subst1_single : t2:T H0:subst0 i v (TLRef n) t2 ⇒
                the thesis becomes 
                or
                  eq T t2 (TLRef n)
                  land (eq nat n i) (eq T t2 (lift (S n) O v))
                   by (subst0_gen_lref . . . . H0)
                   we proved land (eq nat n i) (eq T t2 (lift (S n) O v))
                   we proceed by induction on the previous result to prove 
                      or
                        eq T t2 (TLRef n)
                        land (eq nat n i) (eq T t2 (lift (S n) O v))
                      case conj : H1:eq nat n i H2:eq T t2 (lift (S n) O v) ⇒
                         the thesis becomes 
                         or
                           eq T t2 (TLRef n)
                           land (eq nat n i) (eq T t2 (lift (S n) O v))
                            by (conj . . H1 H2)
                            we proved land (eq nat n i) (eq T t2 (lift (S n) O v))
                            by (or_intror . . previous)

                               or
                                 eq T t2 (TLRef n)
                                 land (eq nat n i) (eq T t2 (lift (S n) O v))

                      or
                        eq T t2 (TLRef n)
                        land (eq nat n i) (eq T t2 (lift (S n) O v))
          we proved 
             or
               eq T x (TLRef n)
               land (eq nat n i) (eq T x (lift (S n) O v))
       we proved 
          ∀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)))