proposition: Lemma gmerge_in m m' y `{!Ok m, !Ok m'} : y ∈ (gmerge m m') -> y ∈ m \/ y ∈ m'.
proof: Proof. functional induction (gmerge m m'); intros H; try factornode m2; invok. - right. apply find_in. generalize (in_find H). destruct (@mapr_f0 y m2) as (y' & ? & ->); trivial. intros A B. rewrite B in A. now elim A. - left. apply find_in. generalize (in_find H). destruct (@mapl_f0 y m2) as (y' & ? & ->); trivial. intros A B. rewrite B in A. now elim A. - rewrite join_in in *. revert IHt2 IHt0 H. cleansplit. generalize (@split_ok_l _ m2 x1 _) (@split_ok_r _ m2 x1 _). rewrite split_in_r, split_in_l; intuition_in. - rewrite concat_in in *. revert IHt2 IHt0 H; cleansplit. generalize (@split_ok_l _ m2 x1 _) (@split_ok_r _ m2 x1 _). rewrite split_in_r, split_in_l; intuition_in. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)