proposition: Lemma merge_spec1n f m m' x `{!Ok m, !Ok m'} : (forall k, f k None None = None) -> exists y, y == x /\ find x (merge f m m') = f y (find x m) (find x m').
proof: Proof. intros Hf. assert (Ok (merge f m m')) by ok. destruct (@mergeL_find f (rev_bindings m) (rev_bindings m') nil x) as (y & Hy & EQ); auto. - rewrite rev_bindings_rev, rev_involutive; now apply bindings_sort. - rewrite rev_bindings_rev, rev_involutive; now apply bindings_sort. - exists y; split; auto. unfold merge in *. rewrite <- !findL_find; auto. rewrite treeify_bindings, EQ. simpl. clear EQ. rewrite rev_bindings_rev, rev_involutive. rewrite rev_bindings_rev, rev_involutive. now destruct f. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)