DEFINITION ex1_arity()
TYPE =
       ∀g:G.(arity g ex1_c ex1_t (ASort O O))
BODY =
Show proof