DEFINITION csubv_refl()
TYPE =
       ∀c:C.(csubv c c)
BODY =
Show proof