diff --git a/coq-actris.opam b/coq-actris.opam
index 08e7857a9583c960e63b6fccd5c0ee71275340ee..c14b302ed59e8b58aeb41d18543cdfa8b7140959 100644
--- a/coq-actris.opam
+++ b/coq-actris.opam
@@ -8,7 +8,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/actris/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/iris/actris.git"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2024-03-12.0.c1e15cdc") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2024-08-16.3.8890e30a") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 4ab5fe0a8fab9a3749ccdcdf11d0a7ea38ec79a5..1212dfbc4d4a5fe71f4f00404351b3c18c9825fc 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -260,7 +260,7 @@ Section channel.
     iIntros "#Hlbl' [Hctx H] !>".
     wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]").
     { iExists (vsl ++ [v]), vsr.
-      rewrite app_length /=.
+      rewrite length_app /=.
       replace (length vsl + 1) with (S (length vsl)) by lia.
       iFrame "#∗". }
     iIntros "_". iApply "HΦ". iExists γl, γr, γlk. eauto 10 with iFrame.
diff --git a/theories/logrel/session_typing_rules.v b/theories/logrel/session_typing_rules.v
index 5cac0e12a7b5810ddbb42c933cd9bbed5631731f..5dfafee1f3d22af759defdff5d2bc19523cf59e5 100644
--- a/theories/logrel/session_typing_rules.v
+++ b/theories/logrel/session_typing_rules.v
@@ -181,7 +181,7 @@ Section session_typing_rules.
     iIntros (Hdom) "!>". iIntros (vs) "$". iApply wp_value.
     iIntros (c) "Hc". wp_lam.
     rewrite -subst_map_singleton.
-    iApply lty_arr_list_spec; [by rewrite fmap_length|].
+    iApply lty_arr_list_spec; [by rewrite length_fmap|].
     iIntros (ws) "H".
     rewrite big_sepL2_fmap_l.
     iDestruct (big_sepL2_length with "H") as %Heq.