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