diff --git a/theories/list.v b/theories/list.v
index 8bcead877d751c06960c8399b6b81eaf11518956..aa5618a1aae6e9feed46be6be3946d8efcd41633 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3770,6 +3770,10 @@ Section zip_with.
     revert k i. induction l; intros [|??] [|?]; f_equal/=; auto.
     by destruct (_ !! _).
   Qed.
+  Lemma lookup_zip_with_Some l k i z :
+    zip_with f l k !! i = Some z
+    ↔ ∃ x y, z = f x y ∧ l !! i = Some x ∧ k !! i = Some y.
+  Proof. rewrite lookup_zip_with. destruct (l !! i), (k !! i); naive_solver. Qed.
   Lemma insert_zip_with l k i x y :
     <[i:=f x y]>(zip_with f l k) = zip_with f (<[i:=x]>l) (<[i:=y]>k).
   Proof. revert i k. induction l; intros [|?] [|??]; f_equal/=; auto. Qed.