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