proposition: Lemma intersection_with_idemp m : (∀ i x, m !! i = Some x → f x x = Some x) → intersection_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)