DEFINITION ty3_gen_abst_abst()
TYPE =
       ∀g:G
         .∀c:C
           .∀u:T
             .∀t1:T
               .∀t2:T
                 .ty3 g c (THead (Bind Abst) u t1) (THead (Bind Abst) u t2)
                   →ex2 T λw:T.ty3 g c u w λ:T.ty3 g (CHead c (Bind Abst) u) t1 t2
BODY =
        assume g: G
        assume c: C
        assume u: T
        assume t1: T
        assume t2: T
        suppose H: ty3 g c (THead (Bind Abst) u t1) (THead (Bind Abst) u t2)
          by (ty3_correct . . . . H)
          we proved ex T λt:T.ty3 g c (THead (Bind Abst) u t2) t
          we proceed by induction on the previous result to prove ex2 T λw:T.ty3 g c u w λ:T.ty3 g (CHead c (Bind Abst) u) t1 t2
             case ex_intro : x:T H0:ty3 g c (THead (Bind Abst) u t2) x ⇒
                the thesis becomes ex2 T λw:T.ty3 g c u w λ:T.ty3 g (CHead c (Bind Abst) u) t1 t2
                   by (ty3_gen_bind . . . . . . H0)
                   we proved 
                      ex3_2
                        T
                        T
                        λt2:T.λ:T.pc3 c (THead (Bind Abst) u t2) x
                        λ:T.λt:T.ty3 g c u t
                        λt2:T.λ:T.ty3 g (CHead c (Bind Abst) u) t2 t2
                   we proceed by induction on the previous result to prove ex2 T λw:T.ty3 g c u w λ:T.ty3 g (CHead c (Bind Abst) u) t1 t2
                      case ex3_2_intro : x0:T x1:T :pc3 c (THead (Bind Abst) u x0) x :ty3 g c u x1 H3:ty3 g (CHead c (Bind Abst) u) t2 x0 ⇒
                         the thesis becomes ex2 T λw:T.ty3 g c u w λ:T.ty3 g (CHead c (Bind Abst) u) t1 t2
                            by (ty3_gen_bind . . . . . . H)
                            we proved 
                               ex3_2
                                 T
                                 T
                                 λt2:T.λ:T.pc3 c (THead (Bind Abst) u t2) (THead (Bind Abst) u t2)
                                 λ:T.λt:T.ty3 g c u t
                                 λt2:T.λ:T.ty3 g (CHead c (Bind Abst) u) t1 t2
                            we proceed by induction on the previous result to prove ex2 T λw:T.ty3 g c u w λ:T.ty3 g (CHead c (Bind Abst) u) t1 t2
                               case ex3_2_intro : x2:T x3:T H4:pc3 c (THead (Bind Abst) u x2) (THead (Bind Abst) u t2) H5:ty3 g c u x3 H6:ty3 g (CHead c (Bind Abst) u) t1 x2 ⇒
                                  the thesis becomes ex2 T λw:T.ty3 g c u w λ:T.ty3 g (CHead c (Bind Abst) u) t1 t2
                                     (H_y) 
                                        by (pc3_gen_abst_shift . . . . H4)
pc3 (CHead c (Bind Abst) u) x2 t2
                                     end of H_y
                                     by (ty3_conv . . . . H3 . . H6 H_y)
                                     we proved ty3 g (CHead c (Bind Abst) u) t1 t2
                                     by (ex_intro2 . . . . H5 previous)
ex2 T λw:T.ty3 g c u w λ:T.ty3 g (CHead c (Bind Abst) u) t1 t2
ex2 T λw:T.ty3 g c u w λ:T.ty3 g (CHead c (Bind Abst) u) t1 t2
ex2 T λw:T.ty3 g c u w λ:T.ty3 g (CHead c (Bind Abst) u) t1 t2
          we proved ex2 T λw:T.ty3 g c u w λ:T.ty3 g (CHead c (Bind Abst) u) t1 t2
       we proved 
          ∀g:G
            .∀c:C
              .∀u:T
                .∀t1:T
                  .∀t2:T
                    .ty3 g c (THead (Bind Abst) u t1) (THead (Bind Abst) u t2)
                      →ex2 T λw:T.ty3 g c u w λ:T.ty3 g (CHead c (Bind Abst) u) t1 t2