proposition: Lemma csp'_wd : forall P : CSetoid_predicate', pred_wd' P.
proof: Proof. intro P. intro x; intros y H H0. elim (csp'_strext P x y H). auto. set (eq_imp_not_ap _ _ _ H0); contradiction. Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid