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