proposition: Lemma eq_spec m m' : eq m m' <-> M.Equiv D.eq m m'.
proof: Proof. unfold eq. rewrite P.eq_spec. unfold M.Equiv. now setoid_rewrite D'.compare_Eq. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)