diff --git a/coq-gpfsl.opam b/coq-gpfsl.opam
index 61db5e555f4186ecf7bda74c0c383e9b168a5dd2..1d0498b06b3faafcd281e20b26c1cdd38b488836 100644
--- a/coq-gpfsl.opam
+++ b/coq-gpfsl.opam
@@ -10,7 +10,7 @@ version: "dev"
 synopsis: "A combination of GPS and FSL in the promising semantics WITHOUT promises"
 
 depends: [
-  "coq-iris"  { (= "dev.2023-10-16.0.4a17223a") | (= "dev") }
+  "coq-iris"  { (= "dev.2023-10-16.2.5e58df61") | (= "dev") }
   "coq-orc11" {= version}
 ]
 
diff --git a/gpfsl-examples/algebra/mono_list_list.v b/gpfsl-examples/algebra/mono_list_list.v
index db2dc67548578e6a780c4c5041acadaccf166801..9dd054f26856a15d6dfac272011b0a01e13b5f4a 100644
--- a/gpfsl-examples/algebra/mono_list_list.v
+++ b/gpfsl-examples/algebra/mono_list_list.v
@@ -173,7 +173,7 @@ Section max_prefix_list_list.
     rewrite /to_max_prefix_list_list !fmap_map_seq !lookup_map_seq Nat.sub_0_r !list_lookup_fmap.
     rewrite !option_guard_True; [|lia..].
     destruct oll as [ll|]; simpl; last by rewrite !right_id.
-    destruct (ll !! i) as [l|]; simpl; last by rewrite !right_id.
+    destruct (ll !! i) as [l|] eqn:EQll; rewrite EQll /=; last by rewrite !right_id.
     destruct (ll1 !! i) as [l1|], (ll2 !! i) as [l2|]; simpl; [|done| |done].
     - rewrite -!Some_op. intros P V EQ%Some_dist_inj. f_equiv.
       move: (max_prefix_list_local_update l1 l2 P n (Some l)). naive_solver.