DEFINITION csuba_refl()
TYPE =
       ∀g:G.∀c:C.(csuba g c c)
BODY =
Show proof