proposition: Lemma subcsetoid_is_CSetoid : is_CSetoid _ subcsetoid_eq subcsetoid_ap.
proof: Proof. apply (Build_is_CSetoid _ subcsetoid_eq subcsetoid_ap). intro x. case x. intros. apply ap_irreflexive. intros x y. case x. case y. intros. exact (ap_symmetric S _ _ X). intros x y. case x. case y. intros; case z. intros. exact (ap_cotransitive S _ _ X scs_elem2). intros x y. case x. case y. intros. exact (ap_tight S scs_elem1 scs_elem0). Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid