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