diff --git a/stdpp/list.v b/stdpp/list.v
index eb7c0e5c5e908797498ffc4dbd2ab31c2de30299..b162808506546d1eef8f9deb7b6c5d6dda2ecdf4 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -5056,18 +5056,18 @@ Section zip.
   Lemma zip_nil_inv l k :
     zip l k = [] ↔ l = [] ∨ k = [].
   Proof. by induction l; induction k; naive_solver. Qed.
-  Lemma lookup_zip_split l k ind e1 e2 :
-    zip l k !! ind = Some (e1, e2) ↔ l !! ind = Some e1 ∧ k !! ind = Some e2.
+  Lemma lookup_zip_split l k i e1 e2 :
+    zip l k !! i = Some (e1, e2) ↔ l !! i = Some e1 ∧ k !! i = Some e2.
   Proof.
-    induction l as [| hd1 tail1 IH1] in k,ind |-*; destruct k as [ | y ys]; simpl;
+    induction l as [| hd1 tail1 IH1] in k,i |-*; destruct k as [ | y ys]; simpl;
       [ naive_solver.. | ].
-    case ind as [| ind']; naive_solver.
+    case i as [| ind']; naive_solver.
   Qed.
-  Lemma lookup_zip_None l k ind :
-    zip l k !! ind = None ↔ l !! ind = None ∨ k !! ind = None.
+  Lemma lookup_zip_None l k i :
+    zip l k !! i = None ↔ l !! i = None ∨ k !! i = None.
   Proof.
-   by induction l as [| hd1 tail1 IH1] in k,ind |-*; destruct k as [ | y ys]; simpl;
-      case ind; naive_solver.
+   by induction l as [| hd1 tail1 IH1] in k,i |-*; destruct k as [ | y ys]; simpl;
+      case i; naive_solver.
   Qed.
 End zip.