proposition: Lemma for_all_spec (f:key->elt->bool) m : for_all f m = List.forallb (fun '(k,e) => f k e) (bindings m).
proof: Proof. induction m; simpl; auto. rewrite bindings_node, forallb_app; simpl. rewrite <- !andb_lazy_alt, andb_assoc, (andb_comm (f _ _)). f_equal; auto. f_equal; auto. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)