proposition: Lemma ap_wdr_unfolded : forall x y z : S, x [#] y -> y [=] z -> x [#] z.
proof: Proof. Proof ap_wdr. Lemma ap_wdl_unfolded : forall x y z : S, x [#] y -> x [=] z -> z [#] y. Proof ap_wdl. Lemma ap_strext : Crel_strext (cs_ap (c:=S)). Proof. intros x1 x2 y1 y2 H. case (ap_cotransitive _ _ _ H x2); intro H0;auto. case (ap_cotransitive _ _ _ H0 y2); intro H1;auto. right; right. now apply ap_symmetric. Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid