proposition: Lemma mapi_spec m : bindings (mapi f m) = List.map (fun '(k,e) => (k,f k e)) (bindings m).
proof: Proof. induction m; simpl; auto. now rewrite !bindings_node, !map_app, IHm1, IHm2. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)