proposition: Lemma neq_imp_notnot_ap : forall x y : S, x [~=] y -> ~ Not (x [#] y).
proof: Proof. intros x y H H0. now apply: H; apply: not_ap_imp_eq. Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid