diff --git a/coq-reloc.opam b/coq-reloc.opam
index 3c9ab2e170d8f8e67c3a49a211865603fa58711c..53b41d097dd72ca9300f450d7f421a487d3cdd7d 100644
--- a/coq-reloc.opam
+++ b/coq-reloc.opam
@@ -6,7 +6,7 @@ bug-reports: "https://gitlab.mpi-sws.org/dfrumin/reloc/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/dfrumin/reloc.git"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2025-02-07.0.d68b4fdb") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2025-03-28.0.fa344cbe") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
 
diff --git a/theories/examples/folly_queue/set.v b/theories/examples/folly_queue/set.v
index 843ea31518a4963b501b3a90a873bacbb6fa09d2..483f4a9b459be486c3b906e4610b3303ec24422f 100644
--- a/theories/examples/folly_queue/set.v
+++ b/theories/examples/folly_queue/set.v
@@ -1,5 +1,5 @@
 From stdpp Require Import base decidable.
-From iris.algebra Require Import numbers cmra excl.
+From iris.algebra Require Import numbers cmra excl stepindex_finite.
 From reloc.prelude Require Import arith.
 
 (* A camera of, potentially, infinite sets. Most of the lemmas are about sets of
diff --git a/theories/examples/stack_helping/helping_wrapper.v b/theories/examples/stack_helping/helping_wrapper.v
index acb7334b9d649a36b102d8c6eae1c1eeb772f6fd..3efaf58529913f1781e3c13f5a237d7b4890cc40 100644
--- a/theories/examples/stack_helping/helping_wrapper.v
+++ b/theories/examples/stack_helping/helping_wrapper.v
@@ -145,10 +145,7 @@ Section offerReg_rules.
         rewrite left_id.
         done.
     }
-    { (** TODO: this is silly *)
-      assert (RightId (≡) (◯ ∅ : authUR offerRegR) (⋅)).
-      { apply (@ucmra_unit_right_id (authUR offerRegR)). }
-      rewrite right_id. iFrame "Hown". }
+    { done. }
     iDestruct "Hown" as "[Ho Hown]".
     rewrite right_id. iFrame.
     assert ({[o := to_agree (v, (γ, k))]} ⋅ to_offer_reg N ≡ to_offer_reg N) as Hfoo.
diff --git a/theories/examples/stack_helping/stack.v b/theories/examples/stack_helping/stack.v
index 38b197177f1615a7d511e6e38e2238795f04620e..5613a506c9bf4cec15bed2f90d38527a7caa55dc 100644
--- a/theories/examples/stack_helping/stack.v
+++ b/theories/examples/stack_helping/stack.v
@@ -171,10 +171,7 @@ Section offerReg_rules.
         rewrite left_id.
         done.
     }
-    { (** TODO: this is silly *)
-      assert (RightId (≡) (◯ ∅ : authUR offerRegR) (⋅)).
-      { apply (@ucmra_unit_right_id (authUR offerRegR)). }
-      rewrite right_id. iFrame "Hown". }
+    { done. }
     iDestruct "Hown" as "[Ho Hown]".
     rewrite right_id. iFrame.
     assert ({[o := to_agree (v, (γ, k))]} ⋅ to_offer_reg N ≡ to_offer_reg N) as Hfoo.