DEFINITION csubc_refl()
TYPE =
       ∀g:G.∀c:C.(csubc g c c)
BODY =
Show proof