proposition: Lemma merge_spec1 f m m' x `{!Ok m, !Ok m'} : (x ∈ m \/ x ∈ m') -> exists y, y == x /\ find x (merge f m m') = f y (find x m) (find x m').
proof: Proof. set (g := fun x o o' => match o,o' with None, None => None | _,_ => f x o o' end). destruct (@merge_spec1n g m m' x) as (y & Hy & EQ); auto. change (merge f) with (merge g). exists y; split; auto. rewrite EQ. destruct (find x m) eqn:F; simpl; auto. destruct (find x m') eqn:F'; simpl; auto. rewrite not_find_iff in F, F'; intuition. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)