DEFINITION pr3_gen_lref()
TYPE =
       ∀c:C
         .∀x:T
           .∀n:nat
             .pr3 c (TLRef n) x
               →(or
                    eq T x (TLRef n)
                    ex3_3
                      C
                      T
                      T
                      λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                      λd:C.λu:T.λv:T.pr3 d u v
                      λ:C.λ:T.λv:T.eq T x (lift (S n) O v))
BODY =
        assume c: C
        assume x: T
        assume n: nat
        suppose H: pr3 c (TLRef n) x
           assume y: T
           suppose H0: pr3 c y x
             we proceed by induction on H0 to prove 
                eq T y (TLRef n)
                  →(or
                       eq T x y
                       ex3_3
                         C
                         T
                         T
                         λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                         λd:C.λu:T.λv:T.pr3 d u v
                         λ:C.λ:T.λv:T.eq T x (lift (S n) O v))
                case pr3_refl : t:T ⇒
                   the thesis becomes 
                   eq T t (TLRef n)
                     →(or
                          eq T t t
                          ex3_3
                            C
                            T
                            T
                            λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                            λd:C.λu:T.λv:T.pr3 d u v
                            λ:C.λ:T.λv:T.eq T t (lift (S n) O v))
                      suppose : eq T t (TLRef n)
                         by (refl_equal . .)
                         we proved eq T t t
                         by (or_introl . . previous)
                         we proved 
                            or
                              eq T t t
                              ex3_3
                                C
                                T
                                T
                                λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                                λd:C.λu:T.λv:T.pr3 d u v
                                λ:C.λ:T.λv:T.eq T t (lift (S n) O v)

                         eq T t (TLRef n)
                           →(or
                                eq T t t
                                ex3_3
                                  C
                                  T
                                  T
                                  λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                                  λd:C.λu:T.λv:T.pr3 d u v
                                  λ:C.λ:T.λv:T.eq T t (lift (S n) O v))
                case pr3_sing : t2:T t1:T H1:pr2 c t1 t2 t3:T H2:pr3 c t2 t3 ⇒
                   the thesis becomes 
                   ∀H4:eq T t1 (TLRef n)
                     .or
                       eq T t3 t1
                       ex3_3
                         C
                         T
                         T
                         λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                         λd:C.λu:T.λv:T.pr3 d u v
                         λ:C.λ:T.λv:T.eq T t3 (lift (S n) O v)
                   (H3) by induction hypothesis we know 
                      eq T t2 (TLRef n)
                        →(or
                             eq T t3 t2
                             ex3_3
                               C
                               T
                               T
                               λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                               λd:C.λu:T.λv:T.pr3 d u v
                               λ:C.λ:T.λv:T.eq T t3 (lift (S n) O v))
                      suppose H4: eq T t1 (TLRef n)
                         (H5) 
                            we proceed by induction on H4 to prove pr2 c (TLRef n) t2
                               case refl_equal : ⇒
                                  the thesis becomes the hypothesis H1
pr2 c (TLRef n) t2
                         end of H5
                         (H6) 
                            by (pr2_gen_lref . . . H5)

                               or
                                 eq T t2 (TLRef n)
                                 ex2_2
                                   C
                                   T
                                   λd:C.λu:T.getl n c (CHead d (Bind Abbr) u)
                                   λ:C.λu:T.eq T t2 (lift (S n) O u)
                         end of H6
                         we proceed by induction on H6 to prove 
                            or
                              eq T t3 (TLRef n)
                              ex3_3
                                C
                                T
                                T
                                λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                                λd:C.λu:T.λv:T.pr3 d u v
                                λ:C.λ:T.λv:T.eq T t3 (lift (S n) O v)
                            case or_introl : H7:eq T t2 (TLRef n) ⇒
                               the thesis becomes 
                               or
                                 eq T t3 (TLRef n)
                                 ex3_3
                                   C
                                   T
                                   T
                                   λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                                   λd:C.λu:T.λv:T.pr3 d u v
                                   λ:C.λ:T.λv:T.eq T t3 (lift (S n) O v)
                                  (H8) 
                                     we proceed by induction on H7 to prove 
                                        eq T (TLRef n) (TLRef n)
                                          →(or
                                               eq T t3 (TLRef n)
                                               ex3_3
                                                 C
                                                 T
                                                 T
                                                 λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                                                 λd:C.λu:T.λv:T.pr3 d u v
                                                 λ:C.λ:T.λv:T.eq T t3 (lift (S n) O v))
                                        case refl_equal : ⇒
                                           the thesis becomes the hypothesis H3

                                        eq T (TLRef n) (TLRef n)
                                          →(or
                                               eq T t3 (TLRef n)
                                               ex3_3
                                                 C
                                                 T
                                                 T
                                                 λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                                                 λd:C.λu:T.λv:T.pr3 d u v
                                                 λ:C.λ:T.λv:T.eq T t3 (lift (S n) O v))
                                  end of H8
                                  by (refl_equal . .)
                                  we proved eq T (TLRef n) (TLRef n)
                                  by (H8 previous)

                                     or
                                       eq T t3 (TLRef n)
                                       ex3_3
                                         C
                                         T
                                         T
                                         λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                                         λd:C.λu:T.λv:T.pr3 d u v
                                         λ:C.λ:T.λv:T.eq T t3 (lift (S n) O v)
                            case or_intror : H7:ex2_2 C T λd:C.λu:T.getl n c (CHead d (Bind Abbr) u) λ:C.λu:T.eq T t2 (lift (S n) O u) ⇒
                               the thesis becomes 
                               or
                                 eq T t3 (TLRef n)
                                 ex3_3
                                   C
                                   T
                                   T
                                   λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                                   λd:C.λu:T.λv:T.pr3 d u v
                                   λ:C.λ:T.λv:T.eq T t3 (lift (S n) O v)
                                  we proceed by induction on H7 to prove 
                                     or
                                       eq T t3 (TLRef n)
                                       ex3_3
                                         C
                                         T
                                         T
                                         λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                                         λd:C.λu:T.λv:T.pr3 d u v
                                         λ:C.λ:T.λv:T.eq T t3 (lift (S n) O v)
                                     case ex2_2_intro : x0:C x1:T H8:getl n c (CHead x0 (Bind Abbr) x1) H9:eq T t2 (lift (S n) O x1) ⇒
                                        the thesis becomes 
                                        or
                                          eq T t3 (TLRef n)
                                          ex3_3
                                            C
                                            T
                                            T
                                            λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                                            λd:C.λu:T.λv:T.pr3 d u v
                                            λ:C.λ:T.λv:T.eq T t3 (lift (S n) O v)
                                           (H11) 
                                              we proceed by induction on H9 to prove pr3 c (lift (S n) O x1) t3
                                                 case refl_equal : ⇒
                                                    the thesis becomes the hypothesis H2
pr3 c (lift (S n) O x1) t3
                                           end of H11
                                           (H12) 
                                              by (getl_drop . . . . . H8)
                                              we proved drop (S n) O c x0
                                              by (pr3_gen_lift . . . . . H11 . previous)
ex2 T λt2:T.eq T t3 (lift (S n) O t2) λt2:T.pr3 x0 x1 t2
                                           end of H12
                                           we proceed by induction on H12 to prove 
                                              or
                                                eq T t3 (TLRef n)
                                                ex3_3
                                                  C
                                                  T
                                                  T
                                                  λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                                                  λd:C.λu:T.λv:T.pr3 d u v
                                                  λ:C.λ:T.λv:T.eq T t3 (lift (S n) O v)
                                              case ex_intro2 : x2:T H13:eq T t3 (lift (S n) O x2) H14:pr3 x0 x1 x2 ⇒
                                                 the thesis becomes 
                                                 or
                                                   eq T t3 (TLRef n)
                                                   ex3_3
                                                     C
                                                     T
                                                     T
                                                     λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                                                     λd:C.λu:T.λv:T.pr3 d u v
                                                     λ:C.λ:T.λv:T.eq T t3 (lift (S n) O v)
                                                    by (ex3_3_intro . . . . . . . . . H8 H14 H13)
                                                    we proved 
                                                       ex3_3
                                                         C
                                                         T
                                                         T
                                                         λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                                                         λd:C.λu:T.λv:T.pr3 d u v
                                                         λ:C.λ:T.λv:T.eq T t3 (lift (S n) O v)
                                                    by (or_intror . . previous)

                                                       or
                                                         eq T t3 (TLRef n)
                                                         ex3_3
                                                           C
                                                           T
                                                           T
                                                           λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                                                           λd:C.λu:T.λv:T.pr3 d u v
                                                           λ:C.λ:T.λv:T.eq T t3 (lift (S n) O v)

                                              or
                                                eq T t3 (TLRef n)
                                                ex3_3
                                                  C
                                                  T
                                                  T
                                                  λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                                                  λd:C.λu:T.λv:T.pr3 d u v
                                                  λ:C.λ:T.λv:T.eq T t3 (lift (S n) O v)

                                     or
                                       eq T t3 (TLRef n)
                                       ex3_3
                                         C
                                         T
                                         T
                                         λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                                         λd:C.λu:T.λv:T.pr3 d u v
                                         λ:C.λ:T.λv:T.eq T t3 (lift (S n) O v)
                         we proved 
                            or
                              eq T t3 (TLRef n)
                              ex3_3
                                C
                                T
                                T
                                λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                                λd:C.λu:T.λv:T.pr3 d u v
                                λ:C.λ:T.λv:T.eq T t3 (lift (S n) O v)
                         by (eq_ind_r . . . previous . H4)
                         we proved 
                            or
                              eq T t3 t1
                              ex3_3
                                C
                                T
                                T
                                λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                                λd:C.λu:T.λv:T.pr3 d u v
                                λ:C.λ:T.λv:T.eq T t3 (lift (S n) O v)

                         ∀H4:eq T t1 (TLRef n)
                           .or
                             eq T t3 t1
                             ex3_3
                               C
                               T
                               T
                               λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                               λd:C.λu:T.λv:T.pr3 d u v
                               λ:C.λ:T.λv:T.eq T t3 (lift (S n) O v)
             we proved 
                eq T y (TLRef n)
                  →(or
                       eq T x y
                       ex3_3
                         C
                         T
                         T
                         λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                         λd:C.λu:T.λv:T.pr3 d u v
                         λ:C.λ:T.λv:T.eq T x (lift (S n) O v))
          we proved 
             ∀y:T
               .pr3 c y x
                 →(eq T y (TLRef n)
                      →(or
                           eq T x y
                           ex3_3
                             C
                             T
                             T
                             λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                             λd:C.λu:T.λv:T.pr3 d u v
                             λ:C.λ:T.λv:T.eq T x (lift (S n) O v)))
          by (insert_eq . . . . previous H)
          we proved 
             or
               eq T x (TLRef n)
               ex3_3
                 C
                 T
                 T
                 λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                 λd:C.λu:T.λv:T.pr3 d u v
                 λ:C.λ:T.λv:T.eq T x (lift (S n) O v)
       we proved 
          ∀c:C
            .∀x:T
              .∀n:nat
                .pr3 c (TLRef n) x
                  →(or
                       eq T x (TLRef n)
                       ex3_3
                         C
                         T
                         T
                         λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                         λd:C.λu:T.λv:T.pr3 d u v
                         λ:C.λ:T.λv:T.eq T x (lift (S n) O v))