proposition: Lemma mapi_spec A B (f:key -> A -> B) (m : t A) : bindings (mapi f m) = List.map (fun '(k,e) => (k, f k e)) (bindings m).
proof: Proof. unfold mapi. rewrite xmapi_spec; simpl; auto. rewrite map_as_mapfilter. f_equiv. now intros (k,e) ? <-. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)