fact: Definition Equiv (A:Type)(eq_elt:A->A->Prop) m m' := (forall k, In k m <-> In k m') /\ (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e').
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface