proposition: Lemma for_all_spec A (f:key->A->bool) m : for_all f m = List.forallb (fun '(k,e) => f k e) (bindings m).
proof: Proof. apply xforall_spec. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)