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