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

                or
                  land (lt (plus n h) d) (eq T t (TLRef (plus n h)))
                  land
                    le (plus d h) (plus n h)
                    eq T t (TLRef (minus (plus n h) 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 (plus n h) d) (eq T t (TLRef (plus 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:lt (plus n h) d H4:eq T t (TLRef (plus n h)) ⇒
                         the thesis becomes eq T t (TLRef n)
                            by (le_plus_l . .)
                            we proved le d (plus d h)
                            by (lt_le_trans . . . H3 previous)
                            we proved lt (plus n h) (plus d h)
                            by (simpl_lt_plus_r . . . previous)
                            we proved lt n d
                            by (lt_le_S . . previous)
                            we proved le (S n) d
                            by (le_false . . . H previous)
                            we proved eq T (TLRef (plus n h)) (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) (plus n h)) (eq T t (TLRef (minus (plus n h) h))) ⇒
                the thesis becomes eq T t (TLRef n)
                   we proceed by induction on H2 to prove eq T t (TLRef n)
                      case conj : :le (plus d h) (plus n h) H4:eq T t (TLRef (minus (plus n h) h)) ⇒
                         the thesis becomes eq T t (TLRef n)
                            by (minus_plus_r . .)
                            we proved eq nat (minus (plus n h) h) n
                            by (f_equal . . . . . previous)
                            we proved eq T (TLRef (minus (plus n h) 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
                .le d n
                  →∀t:T
                       .(eq T (TLRef (plus n h)) (lift h d t))→(eq T t (TLRef n))