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