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