proposition: Lemma Equal_Equivb : forall eqb, (forall e e', eqb e e' = true <-> e = e') -> forall (m m':t elt), m == m' <-> Equivb eqb m m'.
proof: Proof. intros; rewrite Equal_Equiv. apply Equiv_Equivb; auto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)