proposition: Lemma map_spec A B (f:A -> B)(m : t A) : bindings (map f m) = List.map (fun '(k,e) => (k, f e)) (bindings m).
proof: Proof. unfold map. now rewrite mapi_spec. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)