proposition: Lemma merge_spec2 m m' x {Hm : Ok m}{Hm' : Ok m'} : In x (merge m m') -> In x m \/ In x m'.
proof: Proof. intros. destruct H as (e,H). apply find_spec in H; auto using merge_ok. destruct (merge_spec0 x) as (y,(Hy,H')). rewrite H in H'. destruct (find x m) eqn:F. - apply find_spec in F; eauto. - destruct (find x m') eqn:F'. + apply find_spec in F'; eauto. + simpl in H'. discriminate. Qed.
imports: Coq(OrdersFacts OrdersLists)