proposition: Lemma for_all_alt (f:key->elt->bool) m : for_all f m = is_empty (filter (fun k e => negb (f k e)) m).
proof: Proof. apply eq_bool_alt. rewrite for_all_spec, forallb_forall, is_empty_no_binding. setoid_rewrite filter_spec. setoid_rewrite filter_In. split. - intros H x e (IN,E). now rewrite (H (x,e)) in E. - intros H (x,e) IN. specialize (H x e). destruct (f x e) eqn:F; auto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)