DEFINITION pc3_gen_abst()
TYPE =
       ∀c:C
         .∀u1:T
           .∀u2:T
             .∀t1:T
               .∀t2:T
                 .pc3 c (THead (Bind Abst) u1 t1) (THead (Bind Abst) u2 t2)
                   →land (pc3 c u1 u2) ∀b:B.∀u:T.(pc3 (CHead c (Bind b) u) t1 t2)
BODY =
Show proof