diff --git a/CHANGELOG.md b/CHANGELOG.md
index 607fdf3d9218bbec8a0d23bd0c8950d49eb250c8..bea7aca77135425a17d0aca4dc00c35e2557415d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -33,6 +33,8 @@ Coq 8.11 is no longer supported in this version of Iris.
   algorithm.
 * Set `Hint Mode` for the classes `OfeDiscrete`, `Unit`, `CmraMorphism`,
   `rFunctorContractive`, `urFunctorContractive`.
+* Add `max_prefix_list` RA on lists whose composition is only defined when one
+  operand is a prefix of the other. The result is the longer list.
 
 **Changes in `bi`:**
 
diff --git a/_CoqProject b/_CoqProject
index 1ec0701913dc1725f179a23a79c9f1da5999b321..b21005506fcd2bb5f5044b44ef88a9548246641e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -46,6 +46,7 @@ iris/algebra/proofmode_classes.v
 iris/algebra/ufrac.v
 iris/algebra/reservation_map.v
 iris/algebra/dyn_reservation_map.v
+iris/algebra/max_prefix_list.v
 iris/algebra/lib/excl_auth.v
 iris/algebra/lib/frac_auth.v
 iris/algebra/lib/ufrac_auth.v
@@ -170,7 +171,6 @@ iris_heap_lang/lib/arith.v
 iris_heap_lang/lib/array.v
 
 iris_staging/algebra/list.v
-iris_staging/algebra/max_prefix_list.v
 iris_staging/algebra/mono_list.v
 iris_staging/base_logic/algebra.v
 iris_staging/base_logic/mono_list.v
diff --git a/iris_staging/algebra/max_prefix_list.v b/iris/algebra/max_prefix_list.v
similarity index 97%
rename from iris_staging/algebra/max_prefix_list.v
rename to iris/algebra/max_prefix_list.v
index 30f35f7c254a99cfcf29cd2cbbbdc7561290c877..3643c1d83310810f58d7f9fc76dd75579eb70b16 100644
--- a/iris_staging/algebra/max_prefix_list.v
+++ b/iris/algebra/max_prefix_list.v
@@ -1,6 +1,6 @@
-(* This file is still experimental. See its tracking issue
-https://gitlab.mpi-sws.org/iris/iris/-/issues/415 for details on remaining
-issues before stabilization. *)
+(** Defines an RA on lists whose composition is only defined when one operand is
+a prefix of the other. The result is the longer list.
+In particular, the core is the identity function for all elements. *)
 From iris.algebra Require Export agree list gmap updates.
 From iris.algebra Require Import local_updates proofmode_classes.
 From iris.prelude Require Import options.
diff --git a/iris_staging/algebra/mono_list.v b/iris_staging/algebra/mono_list.v
index a417154510c453990964eee1305c82dcb02d4487..c1f6b4b15479a1f3b7e05ff6941d41999e4ee4ee 100644
--- a/iris_staging/algebra/mono_list.v
+++ b/iris_staging/algebra/mono_list.v
@@ -1,8 +1,7 @@
 (* This file is still experimental. See its tracking issue
 https://gitlab.mpi-sws.org/iris/iris/-/issues/415 for details on remaining
 issues before stabilization. *)
-From iris.algebra Require Export auth dfrac.
-From iris.staging.algebra Require Export max_prefix_list.
+From iris.algebra Require Export auth dfrac max_prefix_list.
 From iris.algebra Require Import updates local_updates proofmode_classes.
 From iris.prelude Require Import options.