proposition: Lemma kmap_intersection_with {A} (g : A → A → option A) (m1 m2 : M1 A) : kmap f (intersection_with g m1 m2) = intersection_with g (kmap f m1) (kmap f m2).
proof: Proof. apply kmap_merge. Qed.
imports: Coq(Permutation) stdpp(options)