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

                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
          (H2) consider H_x
          we proceed by induction on H2 to prove P
             case or_introl : H3:land (lt n d) (eq T t (TLRef n)) ⇒
                the thesis becomes P
                   we proceed by induction on H3 to prove P
                      case conj : H4:lt n d :eq T t (TLRef n) ⇒
                         the thesis becomes P
                            consider H4
                            we proved lt n d
                            that is equivalent to le (S n) d
                            by (le_false . . . H previous)
P
P
             case or_intror : H3:land (le (plus d h) n) (eq T t (TLRef (minus n h))) ⇒
                the thesis becomes P
                   we proceed by induction on H3 to prove P
                      case conj : H4:le (plus d h) n :eq T t (TLRef (minus n h)) ⇒
                         the thesis becomes P
                            consider H0
                            we proved lt n (plus d h)
                            that is equivalent to le (S n) (plus d h)
                            by (le_false . . . H4 previous)
P
P
          we proved P
       we proved 
          ∀h:nat
            .∀d:nat
              .∀n:nat
                .le d n
                  →(lt n (plus d h)
                       →∀t:T.(eq T (TLRef n) (lift h d t))→∀P:Prop.P)