DEFINITION pc3_abst_dec()
TYPE =
       ∀g:G
         .∀c:C
           .∀u1:T
             .∀t1:T
               .ty3 g c u1 t1
                 →∀u2:T
                      .∀t2:T
                        .ty3 g c u2 t2
                          →(or
                               ex4_2
                                 T
                                 T
                                 λu:T.λ:T.pc3 c u1 (THead (Bind Abst) u2 u)
                                 λu:T.λv2:T.ty3 g c (THead (Bind Abst) v2 u) t1
                                 λ:T.λv2:T.pr3 c u2 v2
                                 λ:T.λv2:T.nf2 c v2
                               ∀u:T.(pc3 c u1 (THead (Bind Abst) u2 u))→False)
BODY =
Show proof