proposition: Lemma exists_iff (f:key->elt->bool) : Proper (K.eq==>eq==>eq) f -> forall m, exists_ f m = true <-> (exists x e, MapsTo x e m /\ f x e = true).
proof: Proof. intros Hf m. rewrite exists_spec, existsb_exists. split. - intros ((x,e) & IN & E). exists x, e; split; auto. rewrite <- bindings_spec1, InA_alt; now exists (x,e). - intros (x & e & IN & E). rewrite <- bindings_spec1, InA_alt in IN. destruct IN as ((y,e') & (H1,H2) & IN). simpl in *; subst e'. exists (y,e). split; auto. rewrite <- Hf; eauto with *. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)