Lemma CRisCSetoid : is_CSetoid CR (@st_eq CR) CRapart.

Definition CRasCSetoid : CSetoid := makeCSetoid CR _ CRisCSetoid.

Canonical Structure CRasCSetoid.