diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index f065292b944d6504e06c375dfc6094944500ef93..707fea319c8ca26f1ff1bd3b255d8570e21188aa 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1336,6 +1336,10 @@ Proof.
   unfold map_zip_with. rewrite lookup_merge by done.
   by destruct (m1 !! i), (m2 !! i).
 Qed.
+Lemma map_lookup_zip_with_Some {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) i z :
+  map_zip_with f m1 m2 !! i = Some z ↔
+    ∃ x y, z = f x y ∧ m1 !! i = Some x ∧ m2 !! i = Some y.
+Proof. rewrite map_lookup_zip_with. destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
 
 Lemma map_zip_with_empty {A B C} (f : A → B → C) :
   map_zip_with f (∅ : M A) (∅ : M B) = ∅.