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