diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index fc3d6840c844e5b378eedd72203b1ceb92cce4db..d965b6c8c06bf1e7e83babf8f2339e493a9a77ca 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1272,10 +1272,12 @@ Qed.
 Lemma map_zip_with_empty {A B C} (f : A → B → C) :
   map_zip_with f (∅ : M A) (∅ : M B) = ∅.
 Proof. unfold map_zip_with. by rewrite merge_empty by done. Qed.
-
 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. unfold map_zip_with. by erewrite insert_merge by done. Qed.
+Lemma map_zip_with_singleton {A B C} (f : A → B → C) i x y :
+  map_zip_with f ({[ i := x ]} : M A) ({[ i := y ]} : M B) = {[ i := f x y ]}.
+Proof. unfold map_zip_with. by erewrite merge_singleton. Qed.
 
 Lemma map_zip_with_fmap {A' A B' B C} (f : A → B → C)
     (g1 : A' → A) (g2 : B' → B) (m1 : M A') (m2 : M B') :