diff --git a/_CoqProject b/_CoqProject
index 189ee013404786cedf507234a13db5b2c042d2e2..0e17c4c96f8db3a4153a81cbb9adc9e949dda10f 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -8,6 +8,8 @@
 -arg -w -arg -redundant-canonical-projection
 # we use Restart for demoing purposes, sometimes
 -arg -w -arg -undo-batch-mode
+# https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
+-arg -w -arg -notation-incompatible-prefix
 
 # library stuff
 theories/lib/maps.v
diff --git a/semantics.opam b/semantics.opam
index de2143800ac3d1d62220e0e54a38caaa949c7df0..e2227a49df47273718af94fb534439bf3c359ae2 100644
--- a/semantics.opam
+++ b/semantics.opam
@@ -9,10 +9,10 @@ bug-reports: "https://gitlab.mpi-sws.org/FP/semantics-course/issues"
 version: "dev"
 
 depends: [
-  "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
+  "coq" { (>= "8.20" & < "8.21~") | (= "dev") }
   "coq-iris-heap-lang" { (= "dev.2024-12-06.1.72e683c9") | (= "dev") }
-  "coq-equations" { (= "1.3+8.19") | (= "1.3+8.20") }
-  "coq-autosubst" { (= "1.8") | (= "dev") }
+  "coq-equations" { (= "1.3+8.19") | (= "1.3.1+8.20") }
+  "coq-autosubst" { (= "1.9") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/program_logics/program_logic/adequacy.v b/theories/program_logics/program_logic/adequacy.v
index ef05f67f87b89183f057bf5a823d3bfbf15c4d43..7ec04f9911a084a69e66bc88f30a6892db5d7b11 100644
--- a/theories/program_logics/program_logic/adequacy.v
+++ b/theories/program_logics/program_logic/adequacy.v
@@ -48,7 +48,7 @@ Proof.
   iApply (step_fupd_wand with "H"). iIntros ">($ & He2 & -> & ->) !>".
   rewrite !app_nil_r; iFrame.
   iPureIntro; split; first done.
-  rewrite !app_length; simpl; lia.
+  rewrite !length_app; simpl; lia.
 Qed.
 
 Lemma wptp_steps s n es1 es2 κs σ1 σ2 Φs :