DEFINITION ex1_ty3()
TYPE =
       ∀g:G.∀u:T.(ty3 g ex1_c ex1_t u)→∀P:Prop.P
BODY =
Show proof