DEFINITION pr3_gen_cabbr()
TYPE =
       ∀c:C
         .∀t1:T
           .∀t2:T
             .pr3 c t1 t2
               →∀e:C
                    .∀u:T
                      .∀d:nat
                        .getl d c (CHead e (Bind Abbr) u)
                          →∀a0:C
                               .csubst1 d u c a0
                                 →∀a:C
                                      .drop (S O) d a0 a
                                        →∀x1:T.(subst1 d u t1 (lift (S O) d x1))→(ex2 T λx2:T.subst1 d u t2 (lift (S O) d x2) λx2:T.pr3 a x1 x2)
BODY =
        assume c: C
        assume t1: T
        assume t2: T
        suppose H: pr3 c t1 t2
          we proceed by induction on H to prove 
             ∀e:C
               .∀u:T
                 .∀d:nat
                   .getl d c (CHead e (Bind Abbr) u)
                     →∀a0:C
                          .csubst1 d u c a0
                            →∀a:C
                                 .drop (S O) d a0 a
                                   →∀x1:T.(subst1 d u t1 (lift (S O) d x1))→(ex2 T λx2:T.subst1 d u t2 (lift (S O) d x2) λx2:T.pr3 a x1 x2)
             case pr3_refl : t:T ⇒
                the thesis becomes 
                ∀e:C
                  .∀u:T
                    .∀d:nat
                      .getl d c (CHead e (Bind Abbr) u)
                        →∀a0:C
                             .csubst1 d u c a0
                               →∀a:C
                                    .drop (S O) d a0 a
                                      →∀x1:T.∀H3:(subst1 d u t (lift (S O) d x1)).(ex2 T λx2:T.subst1 d u t (lift (S O) d x2) λx2:T.pr3 a x1 x2)
                    assume e: C
                    assume u: T
                    assume d: nat
                    suppose : getl d c (CHead e (Bind Abbr) u)
                    assume a0: C
                    suppose : csubst1 d u c a0
                    assume a: C
                    suppose : drop (S O) d a0 a
                    assume x1: T
                    suppose H3: subst1 d u t (lift (S O) d x1)
                      by (pr3_refl . .)
                      we proved pr3 a x1 x1
                      by (ex_intro2 . . . . H3 previous)
                      we proved ex2 T λx2:T.subst1 d u t (lift (S O) d x2) λx2:T.pr3 a x1 x2

                      ∀e:C
                        .∀u:T
                          .∀d:nat
                            .getl d c (CHead e (Bind Abbr) u)
                              →∀a0:C
                                   .csubst1 d u c a0
                                     →∀a:C
                                          .drop (S O) d a0 a
                                            →∀x1:T.∀H3:(subst1 d u t (lift (S O) d x1)).(ex2 T λx2:T.subst1 d u t (lift (S O) d x2) λx2:T.pr3 a x1 x2)
             case pr3_sing : t0:T t3:T H0:pr2 c t3 t0 t4:T :pr3 c t0 t4 ⇒
                the thesis becomes 
                ∀e:C
                  .∀u:T
                    .∀d:nat
                      .∀H3:getl d c (CHead e (Bind Abbr) u)
                        .∀a0:C
                          .∀H4:csubst1 d u c a0
                            .∀a:C
                              .∀H5:drop (S O) d a0 a
                                .∀x1:T.∀H6:(subst1 d u t3 (lift (S O) d x1)).(ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr3 a x1 x2)
                (H2) by induction hypothesis we know 
                   ∀e:C
                     .∀u:T
                       .∀d:nat
                         .getl d c (CHead e (Bind Abbr) u)
                           →∀a0:C
                                .csubst1 d u c a0
                                  →∀a:C
                                       .drop (S O) d a0 a
                                         →∀x1:T.(subst1 d u t0 (lift (S O) d x1))→(ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr3 a x1 x2)
                    assume e: C
                    assume u: T
                    assume d: nat
                    suppose H3: getl d c (CHead e (Bind Abbr) u)
                    assume a0: C
                    suppose H4: csubst1 d u c a0
                    assume a: C
                    suppose H5: drop (S O) d a0 a
                    assume x1: T
                    suppose H6: subst1 d u t3 (lift (S O) d x1)
                      by (pr2_gen_cabbr . . . H0 . . . H3 . H4 . H5 . H6)
                      we proved ex2 T λx2:T.subst1 d u t0 (lift (S O) d x2) λx2:T.pr2 a x1 x2
                      we proceed by induction on the previous result to prove ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr3 a x1 x2
                         case ex_intro2 : x:T H7:subst1 d u t0 (lift (S O) d x) H8:pr2 a x1 x ⇒
                            the thesis becomes ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr3 a x1 x2
                               by (H2 . . . H3 . H4 . H5 . H7)
                               we proved ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr3 a x x2
                               we proceed by induction on the previous result to prove ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr3 a x1 x2
                                  case ex_intro2 : x0:T H9:subst1 d u t4 (lift (S O) d x0) H10:pr3 a x x0 ⇒
                                     the thesis becomes ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr3 a x1 x2
                                        by (pr3_sing . . . H8 . H10)
                                        we proved pr3 a x1 x0
                                        by (ex_intro2 . . . . H9 previous)
ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr3 a x1 x2
ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr3 a x1 x2
                      we proved ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr3 a x1 x2

                      ∀e:C
                        .∀u:T
                          .∀d:nat
                            .∀H3:getl d c (CHead e (Bind Abbr) u)
                              .∀a0:C
                                .∀H4:csubst1 d u c a0
                                  .∀a:C
                                    .∀H5:drop (S O) d a0 a
                                      .∀x1:T.∀H6:(subst1 d u t3 (lift (S O) d x1)).(ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr3 a x1 x2)
          we proved 
             ∀e:C
               .∀u:T
                 .∀d:nat
                   .getl d c (CHead e (Bind Abbr) u)
                     →∀a0:C
                          .csubst1 d u c a0
                            →∀a:C
                                 .drop (S O) d a0 a
                                   →∀x1:T.(subst1 d u t1 (lift (S O) d x1))→(ex2 T λx2:T.subst1 d u t2 (lift (S O) d x2) λx2:T.pr3 a x1 x2)
       we proved 
          ∀c:C
            .∀t1:T
              .∀t2:T
                .pr3 c t1 t2
                  →∀e:C
                       .∀u:T
                         .∀d:nat
                           .getl d c (CHead e (Bind Abbr) u)
                             →∀a0:C
                                  .csubst1 d u c a0
                                    →∀a:C
                                         .drop (S O) d a0 a
                                           →∀x1:T.(subst1 d u t1 (lift (S O) d x1))→(ex2 T λx2:T.subst1 d u t2 (lift (S O) d x2) λx2:T.pr3 a x1 x2)