proposition: Lemma merge_spec2 m m' x `{!Ok m, !Ok m'} : x ∈ (merge f m m') -> x ∈ m \/ x ∈ m'.
proof: Proof. unfold merge; intros. eapply gmerge_in with (f0:=f); try eassumption; auto using mapo_ok, mapo_find. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)