proposition: Lemma merge_spec2 {A B C}(f:key->option A->option B->option C) : forall m m' x, In x (merge f m m') -> In x m \/ In x m'.
proof: Proof. intros. rewrite <-mem_spec, mem_find in H. unfold merge in H. rewrite xgmerge in H; simpl; auto. rewrite <- 2 mem_spec, 2 mem_find. destruct (find x m); simpl in *; auto. destruct (find x m'); simpl in *; auto. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)