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