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