diff --git a/stdpp/list.v b/stdpp/list.v
index 108ce6e2284560303789c330d65756abb80d5d1d..bd2b29d177ae424e5b2bc0000a252f7a5ecdddb2 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -5051,15 +5051,9 @@ Section zip.
   Lemma zip_nil_inv l k :
     zip l k = [] → l = [] ∨ k = [].
   Proof. intros. by eapply zip_with_nil_inv. Qed.
-  Lemma lookup_zip_Some l k i e1 e2 :
-    zip l k !! i = Some (e1, e2) ↔ l !! i = Some e1 ∧ k !! i = Some e2.
-  Proof.
-    rewrite lookup_zip_with_Some.
-    split; first by intros (x&y&Heq&?&?); inversion Heq; subst;split.
-    intros [->->].
-    do 2 eexists.
-    repeat split; reflexivity.
-  Qed.
+  Lemma lookup_zip_Some l k i x y :
+    zip l k !! i = Some (x, y) ↔ l !! i = Some x ∧ k !! i = Some y.
+  Proof. rewrite lookup_zip_with_Some. naive_solver. Qed.
   Lemma lookup_zip_None l k i :
     zip l k !! i = None ↔ l !! i = None ∨ k !! i = None.
   Proof. by rewrite lookup_zip_with_None. Qed.