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 =
        assume g: G
        assume c1: C
        assume c2: C
        suppose H: csubc g c1 c2
        assume t: T
        assume a: A
        suppose H0: arity g c1 t a
          by (csubc_csuba . . . H)
          we proved csuba g c1 c2
          by (csuba_arity . . . . H0 . previous)
          we proved arity g c2 t a
       we proved ∀g:G.∀c1:C.∀c2:C.(csubc g c1 c2)→∀t:T.∀a:A.(arity g c1 t a)→(arity g c2 t a)