DEFINITION ex2_arity()
TYPE =
       ∀g:G.∀a:A.(arity g ex2_c ex2_t a)→∀P:Prop.P
BODY =
Show proof