proposition: Lemma ap_wdl : Crel_wdl (cs_ap (c:=S)).
proof: Proof. intros x y z H H0. generalize (ap_wdr y x z); intro H1. apply ap_symmetric. now apply H1;[apply ap_symmetric|]. Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid