proposition: Lemma ap_symmetric_unfolded : forall x y : S, x [#] y -> y [#] x.
proof: Proof. Proof ap_symmetric S. Lemma eq_imp_not_ap : forall x y : S, x [=] y -> Not (x [#] y). Proof. intros x y. elim (ap_tight S x y). intros H1 H2. assumption. Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid