proposition: Lemma xmapi_ext {A B}(f g: key -> option A -> option B) : (forall k (o : option A), f k o = g k o) -> forall m i, xmapi f m i = xmapi g m i.
proof: Proof. induction m; intros; simpl; auto. now f_equal. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)