diff --git a/stdpp/list.v b/stdpp/list.v
index bd2b29d177ae424e5b2bc0000a252f7a5ecdddb2..a29f6ecfce98a2c002d7e8ad5d06ba63772d6bb7 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -5039,6 +5039,7 @@ 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.