proposition: Lemma merge_spec1 m m' x {Hm : Ok m}{Hm' : Ok m'} : In x m \/ In x m' -> exists y, X.eq y x /\ find x (merge m m') = f y (find x m) (find x m').
proof: Proof. intros. destruct (merge_spec0 x) as (y,(Hy,H')). exists y; split; [easy|]. rewrite H'. destruct H as [(e,H)|(e,H)]; apply find_spec in H; trivial; rewrite H; simpl; auto. now destruct (find x m). Qed.
imports: Coq(OrdersFacts OrdersLists)