proposition: Lemma map_insert_zip_with {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) i y z : <[i:=f y z]>(map_zip_with f m1 m2) = map_zip_with f (<[i:=y]>m1) (<[i:=z]>m2).
proof: Proof. unfold map_zip_with. by erewrite insert_merge by done. Qed.
imports: Coq(Permutation) stdpp(options)