proposition: Lemma union_with_idemp m : (∀ i x, m !! i = Some x → f x x = Some x) → union_with f m m = m.
proof: Proof. intros. apply merge_idemp. intros i. destruct (m !! i) eqn:?; simpl; eauto. Qed.
imports: Coq(Permutation) stdpp(options)