DEFINITION csubc_csuba()
TYPE =
       ∀g:G.∀c1:C.∀c2:C.(csubc g c1 c2)→(csuba g c1 c2)
BODY =
Show proof