diff --git a/stdpp/list.v b/stdpp/list.v
index 071588c3ba711ad03ac8926eb6dd4e45781968cd..1c12bdeb10043d5b63b419cf978411da8207df65 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -5050,19 +5050,17 @@ Section zip.
     injection 1 as [= <-].
     naive_solver.
   Qed.
-  Lemma zip_length l k :
+  Lemma length_zip l k :
     length (zip l k) = min (length l) (length k).
   Proof. by rewrite length_zip_with. Qed.
-  Lemma zip_nil_implies_list_nil l k :
+  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 :
-    l !! ind = Some e1 →
-    k !! ind = Some e2 →
-    zip l k !! ind = Some(e1, e2).
+    zip l k !! ind = Some (e1, e2) ↔ l !! ind = Some e1 ∧ k !! ind = Some e2.
   Proof.
-    induction l as [| hd1 tail1 IH1] in k,ind |-*; destruct k as [ | y ys]; simpl; [ done.. | ].
-    intros ??.
+    induction l as [| hd1 tail1 IH1] in k,ind |-*; destruct k as [ | y ys]; simpl;
+      [ naive_solver.. | ].
     case ind as [| ind']; naive_solver.
   Qed.
   Lemma lookup_zip_None l k ind :