diff --git a/_CoqProject b/_CoqProject
index 723a4bebeebf76ead8ef9ed97f494a42c1d226b3..40d932068a6fbcef8ff7620e330f483cd4210e40 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -7,8 +7,6 @@
 # Custom flags (to be kept in sync with the dune file at the root of the repo).
 # Fixing this one requires Coq 8.19
 -arg -w -arg -argument-scope-delimiter
-# Fixing this requires Coq 8.20.
--arg -w -arg -deprecated-since-8.20
 # https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
 -arg -w -arg -notation-incompatible-prefix
 
diff --git a/stdpp/list.v b/stdpp/list.v
index cc68e9067b51e7837644201cca60cf351f3940e1..9b25e6d9dc04d99d29a8c2dfb80b33fcca4e85bc 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -881,7 +881,10 @@ Proof. unfold reverse. by rewrite <-!rev_alt, rev_unit. Qed.
 Lemma reverse_app l1 l2 : reverse (l1 ++ l2) = reverse l2 ++ reverse l1.
 Proof. unfold reverse. rewrite <-!rev_alt. apply rev_app_distr. Qed.
 Lemma length_reverse l : length (reverse l) = length l.
-Proof. unfold reverse. rewrite <-!rev_alt. apply rev_length. Qed.
+Proof.
+  induction l as [|x l IH]; [done|].
+  rewrite reverse_cons, length_app, IH. simpl. lia.
+Qed.
 Lemma reverse_involutive l : reverse (reverse l) = l.
 Proof. unfold reverse. rewrite <-!rev_alt. apply rev_involutive. Qed.
 Lemma reverse_lookup l i :