diff --git a/stdpp/list.v b/stdpp/list.v
index f065886d7a279a4bec2c6fd7751ce04815388e2c..071588c3ba711ad03ac8926eb6dd4e45781968cd 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -5035,43 +5035,36 @@ Section zip.
     rewrite <-Forall2_same_length. intros Hlk1 Hlk2. revert l1 k1 Hlk1.
     induction Hlk2; intros ?? [|??????]; simpl; auto.
   Qed.
-
   Lemma elem_of_zip_l x1 x2 l k :
     (x1, x2) ∈ zip l k → x1 ∈ l.
   Proof. intros ?%elem_of_zip_with. naive_solver. Qed.
-
   Lemma elem_of_zip_r x1 x2 l k :
     (x1, x2) ∈ zip l k → x2 ∈ k.
   Proof. intros ?%elem_of_zip_with. naive_solver. Qed.
-
   Lemma lookup_zip i x1 x2 l k :
-  zip l k !! i = Some(x1, x2)  →
-  l !! i = Some x1 ∧ k !! i = Some x2.
+    zip l k !! i = Some(x1, x2)  →
+    l !! i = Some x1 ∧ k !! i = Some x2.
   Proof.
     induction l as [ | x xs IH] in k, i |-*; destruct k as [ | y ys]; simpl; [ done.. | ].
     destruct i as [ | i]; simpl; last by apply IH.
     injection 1 as [= <-].
     naive_solver.
   Qed.
-
   Lemma zip_length 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 :
-  zip l k = [] ↔ 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).
+    l !! ind = Some e1 →
+    k !! ind = Some e2 →
+    zip l k !! ind = Some(e1, e2).
   Proof.
-  induction l as [| hd1 tail1 IH1] in k,ind |-*; destruct k as [ | y ys]; simpl; [ done.. | ].
-  intros ??.
-  case ind as [| ind']; naive_solver.
+    induction l as [| hd1 tail1 IH1] in k,ind |-*; destruct k as [ | y ys]; simpl; [ done.. | ].
+    intros ??.
+    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.