diff --git a/stdpp/list.v b/stdpp/list.v
index 1c12bdeb10043d5b63b419cf978411da8207df65..eb7c0e5c5e908797498ffc4dbd2ab31c2de30299 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -5064,11 +5064,10 @@ Section zip.
     case ind as [| ind']; naive_solver.
   Qed.
   Lemma lookup_zip_None l k ind :
-    length l = length k →
-    zip l k !! ind = None ↔ l !! ind = None ∧ k !! ind = None.
+    zip l k !! ind = None ↔ l !! ind = None ∨ k !! ind = None.
   Proof.
-    induction l as [| hd1 tail1 IH1] in k,ind |-*; destruct k as [ | y ys]; simpl; [ done.. | ].
-    case ind; naive_solver.
+   by induction l as [| hd1 tail1 IH1] in k,ind |-*; destruct k as [ | y ys]; simpl;
+      case ind; naive_solver.
   Qed.
 End zip.