DEFINITION pc3_gen_cabbr()
TYPE =
       ∀c:C
         .∀t1:T
           .∀t2:T
             .pc3 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))→∀x2:T.(subst1 d u t2 (lift (S O) d x2))→(pc3 a x1 x2)
BODY =
        assume c: C
        assume t1: T
        assume t2: T
        suppose H: pc3 c t1 t2
        assume e: C
        assume u: T
        assume d: nat
        suppose H0: getl d c (CHead e (Bind Abbr) u)
        assume a0: C
        suppose H1: csubst1 d u c a0
        assume a: C
        suppose H2: drop (S O) d a0 a
        assume x1: T
        suppose H3: subst1 d u t1 (lift (S O) d x1)
        assume x2: T
        suppose H4: subst1 d u t2 (lift (S O) d x2)
          (H5) consider H
          consider H5
          we proved pc3 c t1 t2
          that is equivalent to ex2 T λt:T.pr3 c t1 t λt:T.pr3 c t2 t
          we proceed by induction on the previous result to prove pc3 a x1 x2
             case ex_intro2 : x:T H6:pr3 c t1 x H7:pr3 c t2 x ⇒
                the thesis becomes pc3 a x1 x2
                   by (pr3_gen_cabbr . . . H7 . . . H0 . H1 . H2 . H4)
                   we proved ex2 T λx2:T.subst1 d u x (lift (S O) d x2) λx2:T.pr3 a x2 x2
                   we proceed by induction on the previous result to prove pc3 a x1 x2
                      case ex_intro2 : x0:T H8:subst1 d u x (lift (S O) d x0) H9:pr3 a x2 x0 ⇒
                         the thesis becomes pc3 a x1 x2
                            by (pr3_gen_cabbr . . . H6 . . . H0 . H1 . H2 . H3)
                            we proved ex2 T λx2:T.subst1 d u x (lift (S O) d x2) λx2:T.pr3 a x1 x2
                            we proceed by induction on the previous result to prove pc3 a x1 x2
                               case ex_intro2 : x3:T H10:subst1 d u x (lift (S O) d x3) H11:pr3 a x1 x3 ⇒
                                  the thesis becomes pc3 a x1 x2
                                     (H12) 
                                        by (subst1_confluence_lift . . . . H10 . H8)
                                        we proved eq T x3 x0
                                        we proceed by induction on the previous result to prove pr3 a x1 x0
                                           case refl_equal : ⇒
                                              the thesis becomes the hypothesis H11
pr3 a x1 x0
                                     end of H12
                                     by (pc3_pr3_t . . . H12 . H9)
pc3 a x1 x2
pc3 a x1 x2
pc3 a x1 x2
          we proved pc3 a x1 x2
       we proved 
          ∀c:C
            .∀t1:T
              .∀t2:T
                .pc3 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))→∀x2:T.(subst1 d u t2 (lift (S O) d x2))→(pc3 a x1 x2)