DEFINITION arity_mono()
TYPE =
       ∀g:G.∀c:C.∀t:T.∀a1:A.(arity g c t a1)→∀a2:A.(arity g c t a2)→(leq g a1 a2)
BODY =
Show proof