proposition: Lemma lookup_intersection_with m1 m2 i : intersection_with f m1 m2 !! i = intersection_with f (m1 !! i) (m2 !! i).
proof: Proof. unfold intersection_with, map_intersection_with. rewrite lookup_merge. by destruct (m1 !! i), (m2 !! i). Qed.
imports: Coq(Permutation) stdpp(options)