proposition: Lemma map_zip_with_singleton {A B C} (f : A → B → C) i x y : map_zip_with f {[ i := x ]} {[ i := y ]} =@{M C} {[ i := f x y ]}.
proof: Proof. unfold map_zip_with. by erewrite merge_singleton. Qed.
imports: Coq(Permutation) stdpp(options)