proposition: Lemma xmapi_spec A B (f: key -> option A -> option B) (i : key) (m : t A) : (forall x, f x None = None) -> bindings (xmapi f m i) = mapfilter (fun '(k,e) => option_map (pair k) (f (i@k) (Some e))) (bindings m).
proof: Proof. revert i. induction m; simpl; intros. easy. rewrite !bindings_node, !mapfilter_app. f_equal. - rewrite IHm1; auto. rewrite map_mapfilter, mapfilter_map; f_equiv. intros a a' <-. destruct a. simpl. now destruct f. - f_equal. + destruct o; simpl. * unfold rev. now destruct f. * now rewrite H. + rewrite IHm2; auto. rewrite map_mapfilter, mapfilter_map; f_equiv. intros a a' <-. destruct a. simpl. now destruct f. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)