DEFINITION ty3_predicative() TYPE = ∀g:G .∀c:C .∀v:T.∀t:T.∀u:T.(ty3 g c (THead (Bind Abst) v t) u)→(pc3 c u v)→∀P:Prop.P BODY =Show proof