proposition: Lemma xgmapi: forall (A B: Type) (f: key -> option A -> option B) (i j : key) (m: t A), (forall k, f k None = None) -> find i (xmapi f m j) = f (j@i) (find i m).
proof: Proof. induction i; intros; destruct m; simpl; rewrite ?IHi; auto. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)