proposition: Lemma for_all_alt2 (f : key -> elt -> bool) m : for_all f m = fold (fun k e b => if f k e then b else false) m true.
proof: Proof. rewrite for_all_spec, fold_spec_right, <- forallb_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)