proposition: Lemma eq_spec m m' : eq m m' <-> Equiv (fun e e' => cmp e e' = Eq) m m'.
proof: Proof. apply compare_Equiv. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)