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