proposition: Lemma union_spec (f:key->elt->elt->option elt) m1 m2 x : Proper (K.eq==>eq==>eq==>eq) f -> find x (union f m1 m2) = match find x m1, find x m2 with | Some e1, Some e2 => f x e1 e2 | o,None | None,o => o end.
proof: Proof. intros Hf. unfold union. rewrite merge_spec1mn; auto. - destruct find, find; auto. - clear x. intros x x' Hx o1 o1' <- o2 o2' <-. destruct o1, o2; auto. apply Hf; auto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)