proposition: Lemma merge_spec2 f m m' x `{!Ok m, !Ok m'} : x ∈ (merge f m m') -> x ∈ m \/ x ∈ m'.
proof: Proof. apply merge_spec2'. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)