cs_ap : relation cs_crr;
cs_proof : is_CSetoid cs_crr cs_eq cs_ap}.
-interpretation "setoid equality"
- 'eq x y = (cic:/matita/algebra/CoRN/Setoids/cs_eq.con _ x y).
+interpretation "setoid equality" 'eq x y = (cs_eq _ x y).
-interpretation "setoid apart"
- 'neq x y = (cic:/matita/algebra/CoRN/Setoids/cs_ap.con _ x y).
+interpretation "setoid apart" 'neq x y = (cs_ap _ x y).
(* visto che sia "ap" che "eq" vanno in Prop e data la "tight-apartness",
"cs_neq" e "ap" non sono la stessa cosa? *)