DEFINITION pc3_gen_sort_abst()
TYPE =
       ∀c:C.∀u:T.∀t:T.∀n:nat.(pc3 c (TSort n) (THead (Bind Abst) u t))→∀P:Prop.P
BODY =
Show proof