proposition: Lemma kmap_zip_with {A B C} (g : A → B → C) (m1 : M1 A) (m2 : M1 B) : kmap f (map_zip_with g m1 m2) = map_zip_with g (kmap f m1) (kmap f m2).
proof: Proof. by apply kmap_merge. Qed.
imports: Coq(Permutation) stdpp(options)