DEFINITION pr2_gen_lref()
TYPE =
       ∀c:C
         .∀x:T
           .∀n:nat
             .pr2 c (TLRef n) x
               →(or
                    eq T x (TLRef n)
                    ex2_2
                      C
                      T
                      λd:C.λu:T.getl n c (CHead d (Bind Abbr) u)
                      λ:C.λu:T.eq T x (lift (S n) O u))
BODY =
        assume c: C
        assume x: T
        assume n: nat
        suppose H: pr2 c (TLRef n) x
           assume y: T
           suppose H0: pr2 c y x
             we proceed by induction on H0 to prove 
                eq T y (TLRef n)
                  →(or
                       eq T x y
                       ex2_2
                         C
                         T
                         λd:C.λu:T.getl n c (CHead d (Bind Abbr) u)
                         λ:C.λu:T.eq T x (lift (S n) O u))
                case pr2_free : c0:C t1:T t2:T H1:pr0 t1 t2 ⇒
                   the thesis becomes 
                   ∀H2:eq T t1 (TLRef n)
                     .or
                       eq T t2 t1
                       ex2_2
                         C
                         T
                         λd:C.λu:T.getl n c0 (CHead d (Bind Abbr) u)
                         λ:C.λu:T.eq T t2 (lift (S n) O u)
                      suppose H2: eq T t1 (TLRef n)
                         (H3) 
                            we proceed by induction on H2 to prove pr0 (TLRef n) t2
                               case refl_equal : ⇒
                                  the thesis becomes the hypothesis H1
pr0 (TLRef n) t2
                         end of H3
                         (h1) 
                            by (refl_equal . .)
                            we proved eq T (TLRef n) (TLRef n)
                            by (or_introl . . previous)

                               or
                                 eq T (TLRef n) (TLRef n)
                                 ex2_2
                                   C
                                   T
                                   λd:C.λu:T.getl n c0 (CHead d (Bind Abbr) u)
                                   λ:C.λu:T.eq T (TLRef n) (lift (S n) O u)
                         end of h1
                         (h2) 
                            by (pr0_gen_lref . . H3)
eq T t2 (TLRef n)
                         end of h2
                         by (eq_ind_r . . . h1 . h2)
                         we proved 
                            or
                              eq T t2 (TLRef n)
                              ex2_2
                                C
                                T
                                λd:C.λu:T.getl n c0 (CHead d (Bind Abbr) u)
                                λ:C.λu:T.eq T t2 (lift (S n) O u)
                         by (eq_ind_r . . . previous . H2)
                         we proved 
                            or
                              eq T t2 t1
                              ex2_2
                                C
                                T
                                λd:C.λu:T.getl n c0 (CHead d (Bind Abbr) u)
                                λ:C.λu:T.eq T t2 (lift (S n) O u)

                         ∀H2:eq T t1 (TLRef n)
                           .or
                             eq T t2 t1
                             ex2_2
                               C
                               T
                               λd:C.λu:T.getl n c0 (CHead d (Bind Abbr) u)
                               λ:C.λu:T.eq T t2 (lift (S n) O u)
                case pr2_delta : c0:C d:C u:T i:nat H1:getl i c0 (CHead d (Bind Abbr) u) t1:T t2:T H2:pr0 t1 t2 t:T H3:subst0 i u t2 t ⇒
                   the thesis becomes 
                   ∀H4:eq T t1 (TLRef n)
                     .or
                       eq T t t1
                       ex2_2
                         C
                         T
                         λd0:C.λu0:T.getl n c0 (CHead d0 (Bind Abbr) u0)
                         λ:C.λu0:T.eq T t (lift (S n) O u0)
                      suppose H4: eq T t1 (TLRef n)
                         (H5) 
                            we proceed by induction on H4 to prove pr0 (TLRef n) t2
                               case refl_equal : ⇒
                                  the thesis becomes the hypothesis H2
pr0 (TLRef n) t2
                         end of H5
                         (H6) 
                            by (pr0_gen_lref . . H5)
                            we proved eq T t2 (TLRef n)
                            we proceed by induction on the previous result to prove subst0 i u (TLRef n) t
                               case refl_equal : ⇒
                                  the thesis becomes the hypothesis H3
subst0 i u (TLRef n) t
                         end of H6
                         by (subst0_gen_lref . . . . H6)
                         we proved land (eq nat n i) (eq T t (lift (S n) O u))
                         we proceed by induction on the previous result to prove 
                            or
                              eq T t (TLRef n)
                              ex2_2
                                C
                                T
                                λd0:C.λu0:T.getl n c0 (CHead d0 (Bind Abbr) u0)
                                λ:C.λu0:T.eq T t (lift (S n) O u0)
                            case conj : H7:eq nat n i H8:eq T t (lift (S n) O u) ⇒
                               the thesis becomes 
                               or
                                 eq T t (TLRef n)
                                 ex2_2
                                   C
                                   T
                                   λd0:C.λu0:T.getl n c0 (CHead d0 (Bind Abbr) u0)
                                   λ:C.λu0:T.eq T t (lift (S n) O u0)
                                  (H9) 
                                     by (eq_ind_r . . . H1 . H7)
getl n c0 (CHead d (Bind Abbr) u)
                                  end of H9
                                  by (refl_equal . .)
                                  we proved eq T (lift (S n) O u) (lift (S n) O u)
                                  by (ex2_2_intro . . . . . . H9 previous)
                                  we proved 
                                     ex2_2
                                       C
                                       T
                                       λd0:C.λu0:T.getl n c0 (CHead d0 (Bind Abbr) u0)
                                       λ:C.λu0:T.eq T (lift (S n) O u) (lift (S n) O u0)
                                  by (or_intror . . previous)
                                  we proved 
                                     or
                                       eq T (lift (S n) O u) (TLRef n)
                                       ex2_2
                                         C
                                         T
                                         λd0:C.λu0:T.getl n c0 (CHead d0 (Bind Abbr) u0)
                                         λ:C.λu0:T.eq T (lift (S n) O u) (lift (S n) O u0)
                                  by (eq_ind_r . . . previous . H8)

                                     or
                                       eq T t (TLRef n)
                                       ex2_2
                                         C
                                         T
                                         λd0:C.λu0:T.getl n c0 (CHead d0 (Bind Abbr) u0)
                                         λ:C.λu0:T.eq T t (lift (S n) O u0)
                         we proved 
                            or
                              eq T t (TLRef n)
                              ex2_2
                                C
                                T
                                λd0:C.λu0:T.getl n c0 (CHead d0 (Bind Abbr) u0)
                                λ:C.λu0:T.eq T t (lift (S n) O u0)
                         by (eq_ind_r . . . previous . H4)
                         we proved 
                            or
                              eq T t t1
                              ex2_2
                                C
                                T
                                λd0:C.λu0:T.getl n c0 (CHead d0 (Bind Abbr) u0)
                                λ:C.λu0:T.eq T t (lift (S n) O u0)

                         ∀H4:eq T t1 (TLRef n)
                           .or
                             eq T t t1
                             ex2_2
                               C
                               T
                               λd0:C.λu0:T.getl n c0 (CHead d0 (Bind Abbr) u0)
                               λ:C.λu0:T.eq T t (lift (S n) O u0)
             we proved 
                eq T y (TLRef n)
                  →(or
                       eq T x y
                       ex2_2
                         C
                         T
                         λd:C.λu:T.getl n c (CHead d (Bind Abbr) u)
                         λ:C.λu:T.eq T x (lift (S n) O u))
          we proved 
             ∀y:T
               .pr2 c y x
                 →(eq T y (TLRef n)
                      →(or
                           eq T x y
                           ex2_2
                             C
                             T
                             λd:C.λu:T.getl n c (CHead d (Bind Abbr) u)
                             λ:C.λu:T.eq T x (lift (S n) O u)))
          by (insert_eq . . . . previous H)
          we proved 
             or
               eq T x (TLRef n)
               ex2_2
                 C
                 T
                 λd:C.λu:T.getl n c (CHead d (Bind Abbr) u)
                 λ:C.λu:T.eq T x (lift (S n) O u)
       we proved 
          ∀c:C
            .∀x:T
              .∀n:nat
                .pr2 c (TLRef n) x
                  →(or
                       eq T x (TLRef n)
                       ex2_2
                         C
                         T
                         λd:C.λu:T.getl n c (CHead d (Bind Abbr) u)
                         λ:C.λu:T.eq T x (lift (S n) O u))