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