proposition: Lemma ap_wdr : Crel_wdr (cs_ap (c:=S)).
proof: Proof. intros x y z H H0. generalize (eq_imp_not_ap _ _ _ H0); intro H1. elim (ap_cotransitive _ _ _ H z); intro H2. assumption. elim H1. now apply: ap_symmetric. Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid