proposition: Lemma merge_spec1 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. unfold merge; intros. edestruct (gmerge_find (f0:=f)) as (y,(Hy,E)); eauto using mapo_ok. - reflexivity. - intros. now apply mapo_find. - intros. now apply mapo_find. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)