proposition: Lemma compare_Equiv cmp (m m':t elt) : compare cmp m m' = Eq <-> Equiv (fun e e' => cmp e e' = Eq) m m'.
proof: Proof. rewrite compare_spec. rewrite list_compare_eq. rewrite bindings_Equiv_eqlistA. split; induction 1; simpl; auto; constructor; auto. - destruct x as (x,e), y as (y,e'). compute. rewrite pair_compare_eq in H. now rewrite compare_eq_iff in H. - destruct x as (x,e), x' as (x',e'). rewrite pair_compare_eq. now rewrite compare_eq_iff. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)