proposition: Lemma intersection_with_comm m1 m2 : (∀ i x y, m1 !! i = Some x → m2 !! i = Some y → f x y = f y x) → intersection_with f m1 m2 = intersection_with f m2 m1.
proof: Proof. intros. apply (merge_comm _). intros i. destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto. Qed.
imports: Coq(Permutation) stdpp(options)