DEFINITION lift_gen_lref_lt()
TYPE =
       ∀h:nat
         .∀d:nat
           .∀n:nat
             .lt n d
               →∀t:T.(eq T (TLRef n) (lift h d t))→(eq T t (TLRef n))
BODY =
        assume h: nat
        assume d: nat
        assume n: nat
        suppose H: lt n d
        assume t: T
        suppose H0: eq T (TLRef n) (lift h d t)
          (H_x) 
             by (lift_gen_lref . . . . H0)

                or
                  land (lt n d) (eq T t (TLRef n))
                  land (le (plus d h) n) (eq T t (TLRef (minus n h)))
          end of H_x
          (H1) consider H_x
          we proceed by induction on H1 to prove eq T t (TLRef n)
             case or_introl : H2:land (lt n d) (eq T t (TLRef n)) ⇒
                the thesis becomes eq T t (TLRef n)
                   we proceed by induction on H2 to prove eq T t (TLRef n)
                      case conj : :lt n d H4:eq T t (TLRef n) ⇒
                         the thesis becomes eq T t (TLRef n)
                            by (refl_equal . .)
                            we proved eq T (TLRef n) (TLRef n)
                            by (eq_ind_r . . . previous . H4)
eq T t (TLRef n)
eq T t (TLRef n)
             case or_intror : H2:land (le (plus d h) n) (eq T t (TLRef (minus n h))) ⇒
                the thesis becomes eq T t (TLRef n)
                   we proceed by induction on H2 to prove eq T t (TLRef n)
                      case conj : H3:le (plus d h) n H4:eq T t (TLRef (minus n h)) ⇒
                         the thesis becomes eq T t (TLRef n)
                            consider H
                            we proved lt n d
                            that is equivalent to le (S n) d
                            by (le_plus_trans . . . previous)
                            we proved le (S n) (plus d h)
                            that is equivalent to lt n (plus d h)
                            by (lt_le_S . . previous)
                            we proved le (S n) (plus d h)
                            by (le_false . . . H3 previous)
                            we proved eq T (TLRef (minus n h)) (TLRef n)
                            by (eq_ind_r . . . previous . H4)
eq T t (TLRef n)
eq T t (TLRef n)
          we proved eq T t (TLRef n)
       we proved 
          ∀h:nat
            .∀d:nat
              .∀n:nat
                .lt n d
                  →∀t:T.(eq T (TLRef n) (lift h d t))→(eq T t (TLRef n))