DEFINITION arity_gen_sort()
TYPE =
       ∀g:G.∀c:C.∀n:nat.∀a:A.(arity g c (TSort n) a)→(leq g a (ASort O n))
BODY =
Show proof