proposition: Lemma merge_spec2' f m m' x : x ∈ (merge f m m') -> x ∈ m \/ x ∈ m'.
proof: Proof. unfold merge, "∈". setoid_rewrite treeify_mapsto. intros H. apply mergeL_in in H. destruct H as [(v,H)|[(v,H)|(v,H)]]. - left. exists v. rewrite rev_bindings_rev, InA_rev in H. now apply bindings_spec1. - right. exists v. rewrite rev_bindings_rev, InA_rev in H. now apply bindings_spec1. - now rewrite InA_nil in H. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)