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