proposition: Lemma map_delete_zip_with {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) i : delete i (map_zip_with f m1 m2) = map_zip_with f (delete i m1) (delete i m2).
proof: Proof. unfold map_zip_with. by rewrite delete_merge. Qed.
imports: Coq(Permutation) stdpp(options)