proposition: Lemma CSetoid_is_CSetoid : is_CSetoid S (cs_eq (r:=S)) (cs_ap (c:=S)).
proof: Proof. Proof cs_proof S. Lemma ap_irreflexive : irreflexive (cs_ap (c:=S)). Proof. elim CSetoid_is_CSetoid; auto. Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid