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 =
Show proof