DEFINITION csubt_refl()
TYPE =
       ∀g:G.∀c:C.(csubt g c c)
BODY =
Show proof