From 02d67bfd0434750b61e818b348e1972d3c2d5c7f Mon Sep 17 00:00:00 2001
From: Kimaya Bedarkar <kbedarka@mpi-sws.org>
Date: Fri, 17 Jan 2025 12:07:29 +0100
Subject: [PATCH] fix

---
 stdpp/list.v | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/stdpp/list.v b/stdpp/list.v
index 1c12bdeb..eb7c0e5c 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.
 
-- 
GitLab