proposition: Lemma for_all_iff (f:key->elt->bool) : Proper (K.eq==>eq==>eq) f -> forall m, for_all f m = true <-> (forall x e, MapsTo x e m -> f x e = true).
proof: Proof. intros Hf m. rewrite for_all_spec, forallb_forall. split. - intros H x e. rewrite <- bindings_spec1, InA_alt. intros ((y,e') & (H1,H2) & IN). simpl in *; subst e'. specialize (H (y,e) IN). simpl in *. rewrite <- Hf; eauto with *. - intros H (x,e) IN. apply H. rewrite <- bindings_spec1, InA_alt. now exists (x,e). Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)