proposition: Lemma Eqdom_Equiv (m m' : t elt) : Eqdom m m' <-> Equiv (fun _ _ => True) m m'.
proof: Proof. unfold Equiv. firstorder. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)