proposition: Lemma exists_alt2 (f : key -> elt -> bool) m : exists_ f m = fold (fun k e b => if f k e then true else b) m false.
proof: Proof. rewrite exists_spec, fold_spec_right, <- existsb_rev. induction (rev (bindings m)) as [|(x,e) l IH]; simpl; auto. unfold uncurry at 1; simpl. destruct f; simpl; auto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)