proposition: Lemma Ccsr_wdr : forall R : CCSetoid_relation, Crel_wdr R.
proof: Proof. intro R. intros x y z H H0. elim (Ccsr_strext R x x y z H);auto. intros [H1|H2]. elim (ap_irreflexive _ _ H1). set (eq_imp_not_ap _ _ _ H0). contradiction. Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid