proposition: Lemma exists_alt (f:key->elt->bool) m : exists_ f m = negb (is_empty (filter f m)).
proof: Proof. apply eq_bool_alt. rewrite exists_spec, existsb_exists, negb_true_iff, not_empty_has_binding. setoid_rewrite filter_spec. setoid_rewrite filter_In. split. - intros ((x,e) & IN & E). firstorder. - intros (x & e & IN & E). now exists (x,e). Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)