DEFINITION ty3_inv_lref_lref_nf2()
TYPE =
       ∀g:G
         .∀c:C
           .∀i:nat
             .∀j:nat
               .ty3 g c (TLRef i) (TLRef j)
                 →(nf2 c (TLRef i))→(nf2 c (TLRef j))→(lt i j)
BODY =
        assume g: G
        assume c: C
        assume i: nat
        assume j: nat
        suppose H: ty3 g c (TLRef i) (TLRef j)
        suppose H0: nf2 c (TLRef i)
        suppose H1: nf2 c (TLRef j)
          (H_x) 
             by (ty3_inv_lref_nf2 . . . . H H0 H1)
ex T λu0:T.eq T (TLRef j) (lift (S i) O u0)
          end of H_x
          (H2) consider H_x
          we proceed by induction on H2 to prove lt i j
             case ex_intro : x:T H3:eq T (TLRef j) (lift (S i) O x) ⇒
                the thesis becomes lt i j
                   (H_x0) 
                      by (lift_gen_lref . . . . H3)

                         or
                           land (lt j O) (eq T x (TLRef j))
                           land (le (plus O (S i)) j) (eq T x (TLRef (minus j (S i))))
                   end of H_x0
                   (H4) consider H_x0
                   consider H4
                   we proved 
                      or
                        land (lt j O) (eq T x (TLRef j))
                        land (le (plus O (S i)) j) (eq T x (TLRef (minus j (S i))))
                   that is equivalent to 
                      or
                        land (lt j O) (eq T x (TLRef j))
                        land (le (S i) j) (eq T x (TLRef (minus j (S i))))
                   we proceed by induction on the previous result to prove lt i j
                      case or_introl : H5:land (lt j O) (eq T x (TLRef j)) ⇒
                         the thesis becomes lt i j
                            we proceed by induction on H5 to prove lt i j
                               case conj : H6:lt j O :eq T x (TLRef j) ⇒
                                  the thesis becomes lt i j
                                     by (lt_x_O . H6 .)
lt i j
lt i j
                      case or_intror : H5:land (le (S i) j) (eq T x (TLRef (minus j (S i)))) ⇒
                         the thesis becomes lt i j
                            we proceed by induction on H5 to prove lt i j
                               case conj : H6:le (S i) j :eq T x (TLRef (minus j (S i))) ⇒
                                  the thesis becomes lt i j
                                     consider H6
                                     we proved le (S i) j
lt i j
lt i j
lt i j
          we proved lt i j
       we proved 
          ∀g:G
            .∀c:C
              .∀i:nat
                .∀j:nat
                  .ty3 g c (TLRef i) (TLRef j)
                    →(nf2 c (TLRef i))→(nf2 c (TLRef j))→(lt i j)