proposition: Lemma Equal_Equiv (m m' : t elt) : m == m' <-> Equiv Logic.eq m m'.
proof: Proof. rewrite Equal_mapsto_iff. split; intros. - split. + split; intros (e,Hin); exists e; [rewrite <- H|rewrite H]; auto. + intros; apply mapsto_fun with m k; auto; rewrite H; auto. - split; intros H'. + destruct H. assert (Hin : In k m') by (rewrite <- H; exists e; auto). destruct Hin as (e',He'). rewrite (H0 k e e'); auto. + destruct H. assert (Hin : In k m) by (rewrite H; exists e; auto). destruct Hin as (e',He'). rewrite <- (H0 k e' e); auto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)