DEFINITION csubc_arity_conf()
TYPE =
       ∀g:G.∀c1:C.∀c2:C.(csubc g c1 c2)→∀t:T.∀a:A.(arity g c1 t a)→(arity g c2 t a)
BODY =
Show proof