diff --git a/coq-diaframe.opam b/coq-diaframe.opam
index 545edaf617ea7750678975120e389e8434874055..1a7a7da2979b12afc89c791e27bfea13329648d1 100644
--- a/coq-diaframe.opam
+++ b/coq-diaframe.opam
@@ -7,7 +7,7 @@ authors: "Ike Mulder <me@ikemulder.nl>"
 homepage: "https://gitlab.mpi-sws.org/iris/diaframe/"
 bug-reports: "https://gitlab.mpi-sws.org/iris/diaframe/-/issues"
 depends: [
-  "coq-iris" { (>= "dev.2024-08-16.3.8890e30a" & <= "dev.2025-01-31.0.1bb4eba3" ) | = "dev" | = "4.1.0" }
+  "coq-iris" { (>= "dev.2025-03-28.0.fa344cbe" & <= "dev.2025-03-31.0.017605dd" ) | = "dev" }
   "coq" { >= "8.19" & < "8.21~" }
 ]
 build: [make "-j%{jobs}%" "diaframe"]
diff --git a/diaframe/hint_search/instances_base.v b/diaframe/hint_search/instances_base.v
index 4747a49b2f6ab1275dfe6bba9f0edfef311b0f15..e430d107fa08042104761b034c4d9873f4e86dad 100644
--- a/diaframe/hint_search/instances_base.v
+++ b/diaframe/hint_search/instances_base.v
@@ -74,10 +74,10 @@ Section biabd_instances.
       iApply "H". by iRight.
   Qed.
 
-  Global Instance biabd_emp_valid {TTl TTr} p P Q M R S :
-    AsEmpValid (BiAbd (TTl := TTl) (TTr := TTr) p P Q M R S) (∀.. (ttl : TTl), □?p P ∗ (tele_app R ttl) -∗ M $ ∃.. (ttr : TTr), tele_app Q ttr ∗ tele_app (tele_app S ttl) ttr).
+  Global Instance biabd_emp_valid {TTl TTr} d p P Q M R S :
+    AsEmpValid d (BiAbd (TTl := TTl) (TTr := TTr) p P Q M R S) (∀.. (ttl : TTl), □?p P ∗ (tele_app R ttl) -∗ M $ ∃.. (ttr : TTr), tele_app Q ttr ∗ tele_app (tele_app S ttl) ttr).
   Proof.
-    split.
+    split => _.
     - rewrite /BiAbd /= => /tforall_forall HPQ.
       iIntros (ttl) "HPR". rewrite HPQ //.
     - rewrite /BiAbd tforall_forall /= => HPQ ttl.
@@ -124,10 +124,10 @@ Section abduction_instances.
     HINT1 P ✱ [ emp ] ⊫ [id]; P | 50.
   Proof. by rewrite /Abduct /= right_id. Qed.
 
-  Global Instance abduct_emp_valid {TT} p P Q M R :
-    AsEmpValid (Abduct (TT := TT) p P Q M R) (□?p P ∗ R -∗ M $ ∃.. (tt : TT), tele_app Q tt)%I.
+  Global Instance abduct_emp_valid {TT} d p P Q M R :
+    AsEmpValid d (Abduct (TT := TT) p P Q M R) (□?p P ∗ R -∗ M $ ∃.. (tt : TT), tele_app Q tt)%I.
   Proof.
-    split; rewrite /Abduct /=.
+    split => _; rewrite /Abduct /=.
     - move => -> //. iIntros "$".
     - move => HPQ. iApply HPQ.
   Qed.
diff --git a/diaframe/lib/do_lob.v b/diaframe/lib/do_lob.v
index 764ae6a19107a482f3180fc2e01cf9f4f7014525..cea460ddc7633fe117e2f40f48ef62ec27343c23 100644
--- a/diaframe/lib/do_lob.v
+++ b/diaframe/lib/do_lob.v
@@ -1,4 +1,4 @@
-From iris.bi Require Export bi telescopes lib.laterable lib.fixpoint.
+From iris.bi Require Export bi telescopes lib.laterable lib.fixpoint_mono.
 From iris.proofmode Require Import proofmode environments.
 From diaframe Require Import proofmode_base utils_ltac2.
 
diff --git a/diaframe/lib/greatest_fixpoint.v b/diaframe/lib/greatest_fixpoint.v
index 47603039c5b541fc29e9a084782c327aa071d133..20a5318bdd078f0cbec172c5bafd65d4ac32ca14 100644
--- a/diaframe/lib/greatest_fixpoint.v
+++ b/diaframe/lib/greatest_fixpoint.v
@@ -1,4 +1,4 @@
-From iris.bi Require Export bi telescopes lib.fixpoint.
+From iris.bi Require Export bi telescopes lib.fixpoint_mono.
 From iris.proofmode Require Import proofmode environments classes_make.
 From diaframe Require Import proofmode_base.
 
diff --git a/diaframe/lib/own/proofmode_instances.v b/diaframe/lib/own/proofmode_instances.v
index 6622ed9e901a72c801918d39f815cb1057a52f1f..1ad8d44ad5b0ff86593aaaa8d14c06a035a169cf 100644
--- a/diaframe/lib/own/proofmode_instances.v
+++ b/diaframe/lib/own/proofmode_instances.v
@@ -6,7 +6,8 @@ From diaframe.lib.own Require Import proofmode_classes.
 
 (* TODO: Remove this file once https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/771 is merged *)
 
-Local Instance includedI_into_pure `{CmraDiscrete A} (a b : A) {Σ} : IntoPure (PROP := iPropI Σ) (a ≼ b)%I (a ≼ b).
+Local Instance includedI_into_pure `{@CmraDiscrete natSI A} (a b : A) {Σ} :
+  IntoPure (PROP := iPropI Σ) (a ≼ b)%I (a ≼ b).
 Proof.
   rewrite /IntoPure. iDestruct 1 as (c) "%"; iPureIntro.
   by eexists.
@@ -383,7 +384,7 @@ Section recursive.
     by iRewrite "Ha".
   Qed.
   Global Instance sum_inl_inr_invalid_op {A B : cmra} (a : A) (b : B) Σ :
-    IsValidOp (CsumBot) (Cinl (B := B) a) (Cinr (A := A) b) Σ False.
+    IsValidOp (CsumInvalid) (Cinl (B := B) a) (Cinr (A := A) b) Σ False.
   Proof. 
     split; rewrite /op /= /cmra_op //=; eauto. (* TODO: need proper access to unsealing lemma's *)
     uPred_primitive.unseal.
@@ -391,7 +392,7 @@ Section recursive.
     rewrite /validN /= /cmra_validN //=.
   Qed.
   Global Instance sum_inr_inl_invalid_op {A B : cmra} (a : A) (b : B) Σ :
-    IsValidOp (CsumBot) (Cinr (A := B) a) (Cinl (B := A) b) Σ False.
+    IsValidOp (CsumInvalid) (Cinr (A := B) a) (Cinl (B := A) b) Σ False.
   Proof. 
     split; rewrite /op /= /cmra_op //=; eauto.
     uPred_primitive.unseal.
@@ -660,7 +661,7 @@ Section recursive.
   Qed.
 
   Global Instance excl_valid_op {O : ofe} (a1 a2 : excl O) Σ:
-    IsValidOp ExclBot a1 a2 Σ False%I.
+    IsValidOp ExclInvalid a1 a2 Σ False%I.
   Proof. split; rewrite excl_validI /=; eauto. Qed.
   Global Instance excl_included_merge {O : ofe} (o1 o2 : excl O) {Σ} :
     IsIncludedMerge o1 o2 (Σ := Σ) False%I.
@@ -1029,4 +1030,4 @@ Section recursive.
       iSplit => //.
   Qed.
 
-End recursive.
\ No newline at end of file
+End recursive.
diff --git a/diaframe/lib/own_hints.v b/diaframe/lib/own_hints.v
index eab37a4a2e269a380baf56f86e3fabd4f9eec78a..59aacd25d5d17eb2b13ed0a2a8639d261f98f666 100644
--- a/diaframe/lib/own_hints.v
+++ b/diaframe/lib/own_hints.v
@@ -3,12 +3,12 @@ From iris.algebra Require Import local_updates excl auth lib.frac_auth csum.
 (* Diaframe hint library aimed at automatically deriving good hints for owned propositions.
    Supports most of the (recursive) building blocks for cmra's found in iris.algebra *)
 
-Class FindLocalUpdate {A : cmra} (x x' y y' : A) (φ : Prop) :=
+Class FindLocalUpdate {SI : sidx} {A : cmra} (x x' y y' : A) (φ : Prop) :=
   find_local_update : φ → (x, y) ~l~> (x', y').
-Global Hint Mode FindLocalUpdate ! ! ! - - - : typeclass_instances.
+Global Hint Mode FindLocalUpdate + ! ! ! - - - : typeclass_instances.
 
 Section base_local_updates.
-  Lemma find_local_update_incomparable {A : ucmra} (x x' : A) :
+  Lemma find_local_update_incomparable {SI : sidx} {A : ucmra} (x x' : A) :
     Cancelable x →
     (* This is needed to find things like 
         (Some (Cinl x), Some (Cinl x)) ~l~> (Some (Cinr x'), Some (Cinr x')) 
@@ -34,7 +34,7 @@ Section base_local_updates.
     but its useful/fast for cmras which do not have that: nat, positive, GSet, GMultiset. how to improve..?
   Proof. done. Qed. *)
 
-  Global Instance find_local_update_from_prod_both {A B : cmra} (x1 x1' y1 y1' : A) (x2 x2' y2 y2' : B) φ1 φ2 :
+  Global Instance find_local_update_from_prod_both {SI : sidx} {A B : cmra} (x1 x1' y1 y1' : A) (x2 x2' y2 y2' : B) φ1 φ2 :
     FindLocalUpdate x1 x1' y1 y1' φ1 →
     FindLocalUpdate x2 x2' y2 y2' φ2 →
     FindLocalUpdate (x1, x2) (x1', x2') (y1, y2) (y1', y2') (φ1 ∧ φ2) | 150.
@@ -43,7 +43,7 @@ Section base_local_updates.
     apply prod_local_update' => //.
   Qed.
 
-  Global Instance find_local_update_from_prod_left {A B : cmra} (x1 x1' y1 y1' : A) (x2 y2 : B) φ :
+  Global Instance find_local_update_from_prod_left {SI : sidx} {A B : cmra} (x1 x1' y1 y1' : A) (x2 y2 : B) φ :
     FindLocalUpdate x1 x1' y1 y1' φ →
     FindLocalUpdate (x1, x2) (x1', x2) (y1, y2) (y1', y2) φ | 160.
   Proof.
@@ -51,7 +51,7 @@ Section base_local_updates.
     apply prod_local_update_1 => //.
   Qed.
 
-  Global Instance find_local_update_from_prod_right {A B : cmra} (x1 y1 : A) (x2 x2' y2 y2' : B) φ :
+  Global Instance find_local_update_from_prod_right {SI : sidx} {A B : cmra} (x1 y1 : A) (x2 x2' y2 y2' : B) φ :
     FindLocalUpdate x2 x2' y2 y2' φ →
     FindLocalUpdate (x1, x2) (x1, x2') (y1, y2) (y1, y2') φ | 160.
   Proof.
@@ -59,32 +59,32 @@ Section base_local_updates.
     apply prod_local_update_2 => //.
   Qed.
 
-  Global Instance find_local_update_some {A : cmra} (x x' y y' : A) φ :
+  Global Instance find_local_update_some {SI : sidx} {A : cmra} (x x' y y' : A) φ :
     FindLocalUpdate x x' y y' φ →
     FindLocalUpdate (Some x) (Some x') (Some y) (Some y') φ | 210.
   Proof. move => H /H H'. by apply option_local_update. Qed.
 
-  Global Instance find_local_update_exclusive {A : ofe} (x x' y : exclR A) :
+  Global Instance find_local_update_exclusive {SI : sidx} {A : ofe} (x x' y : exclR A) :
     FindLocalUpdate x x' y x' (✓ x') | 150.
   Proof. move => Hx1 Hx2. by apply exclusive_local_update. Qed.
 
-  Global Instance sum_inl_find_local_update {A1 A2 : cmra} (x x' y y' : A1) φ :
+  Global Instance sum_inl_find_local_update {SI : sidx} {A1 A2 : cmra} (x x' y y' : A1) φ :
     FindLocalUpdate x x' y y' φ →
     FindLocalUpdate (Cinl (B:=A2) x) (Cinl x') (Cinl y) (Cinl y') φ | 150.
   Proof. move => H /H H'. by apply csum_local_update_l. Qed.
 
-  Global Instance sum_inr_find_local_update {A1 A2 : cmra} (x x' y y' : A1) φ :
+  Global Instance sum_inr_find_local_update {SI : sidx} {A1 A2 : cmra} (x x' y y' : A1) φ :
     FindLocalUpdate x x' y y' φ →
     FindLocalUpdate (Cinr (A:=A2) x) (Cinr x') (Cinr y) (Cinr y') φ | 150.
   Proof. move => H /H H'. by apply csum_local_update_r. Qed.
 
-  Global Instance sum_inl_inr_swap_local_update {A1 A2 : cmra} (x : A1) (x' : A2) :
+  Global Instance sum_inl_inr_swap_local_update {SI : sidx} {A1 A2 : cmra} (x : A1) (x' : A2) :
     Cancelable (Some $ Cinl (B :=A2) x) →
     FindLocalUpdate (Some $ Cinl (B:=A2) x) (Some $ Cinr (A:=A1) x') (Some $ Cinl (B:=A2) x)
          (Some $ Cinr (A:=A1) x') (✓ x') | 160.
   Proof. eapply (find_local_update_incomparable (A := optionUR $ csumR A1 A2)). Qed.
 
-  Global Instance sum_inr_inl_swap_local_update {A1 A2 : cmra} (x : A1) (x' : A2) :
+  Global Instance sum_inr_inl_swap_local_update {SI : sidx} {A1 A2 : cmra} (x : A1) (x' : A2) :
     Cancelable (Some $ Cinr (A :=A2) x) →
     FindLocalUpdate (Some $ Cinr (A:=A2) x) (Some $ Cinl (B:=A1) x') (Some $ Cinr (A:=A2) x)
          (Some $ Cinl (B:=A1) x') (✓ x') | 160.
@@ -92,10 +92,11 @@ Section base_local_updates.
 
 End base_local_updates.
 
-Class AsCmraUnit {A : ucmra} (x : A) :=
+Class AsCmraUnit {SI : sidx} {A : ucmra} (x : A) :=
   as_cmra_unit : x = ε.
 
 Section base_as_unit.
+  Context {SI : sidx}.
   Implicit Types A : ucmra.
 
   Global Instance unit_as_unit {A} : AsCmraUnit (A := A) ε | 99.
@@ -117,6 +118,8 @@ From iris.algebra Require Import numbers.
 From diaframe Require Import solve_defs util_classes.
 
 Section number_updates.
+  Context {SI : sidx}.
+
   Global Instance natO_local_update (x x' y : nat) :
     FindLocalUpdate x x' y (x' + y - x) (x ≤ x' + y) | 150.
   Proof.
@@ -233,6 +236,7 @@ End number_updates.
 From iris.algebra Require Import gset.
 
 Section set_updates.
+  Context {SI : sidx}.
   Context `{Countable K}.
   Implicit Types X Y : gset K.
 
@@ -335,7 +339,7 @@ From stdpp Require Import telescopes.
 Section other.
 
   Global Instance excl_inhabited {A : ofe} : Inhabited (exclR A).
-  Proof. split. by apply ExclBot. Qed.
+  Proof. split. by apply ExclInvalid. Qed.
 
   Global Arguments option_unit_instance /.
 
@@ -998,14 +1002,14 @@ Section validity.
       by iRewrite "Ha".
     Qed.
     Global Instance sum_inl_inr_invalid_op {A B : cmra} (a : A) (b : B) Σ :
-      IsValidOp (CsumBot) (Cinl (B := B) a) (Cinr (A := A) b) Σ False.
+      IsValidOp (CsumInvalid) (Cinl (B := B) a) (Cinr (A := A) b) Σ False.
     Proof. 
       split; rewrite /op /= /cmra_op //=; eauto.
       rewrite uPred_cmra_valid_eq /= /uPred_cmra_valid_def /=.
       rewrite /validN /= /cmra_validN //=.
     Qed.
     Global Instance sum_inr_inl_invalid_op {A B : cmra} (a : A) (b : B) Σ :
-      IsValidOp (CsumBot) (Cinr (A := B) a) (Cinl (B := A) b) Σ False.
+      IsValidOp (CsumInvalid) (Cinr (A := B) a) (Cinl (B := A) b) Σ False.
     Proof. 
       split; rewrite /op /= /cmra_op //=; eauto.
       rewrite uPred_cmra_valid_eq /= /uPred_cmra_valid_def /=.
@@ -1482,7 +1486,7 @@ Section validity.
     Qed.
 
     Global Instance excl_valid_op {O : ofe} (a1 a2 : excl O) Σ:
-      IsValidOp ExclBot a1 a2 Σ False%I.
+      IsValidOp ExclInvalid a1 a2 Σ False%I.
     Proof. split; rewrite excl_validI /=; eauto. Qed. *)
     Lemma excl_subtract {O : ofe} (o1 o2 : O) : (* this one is bad for recursive instances *)
       TCIf (SolveSepSideCondition (¬ (o1 ≡ o2))) False TCTrue →
diff --git a/diaframe/steps/verify_tac.v b/diaframe/steps/verify_tac.v
index e6c8234ebafd577390280f565dbd012d78450d2a..98d538b6cfdd6a87046fc09e453da215b52d7523 100644
--- a/diaframe/steps/verify_tac.v
+++ b/diaframe/steps/verify_tac.v
@@ -15,8 +15,8 @@ Ltac inside_step :=
   lazymatch goal with
   | |- subG _ _ → _ => solve_inG
   | |- IntoWand2 _ _ _ _ => rewrite /IntoWand2 /=; iStartProof
-  | |- forall n : nat, respectful (dist n) (dist n) ?P ?P => solve_proper
-  | |- forall n : nat, respectful (dist_later n) (dist n) ?P ?P => solve_contractive
+  | |- respectful (dist ?n) (dist ?n) ?P ?P => solve_proper
+  | |- respectful (dist_later ?n) (dist ?n) ?P ?P => solve_contractive
   | |- (∀ a, _) => 
     intros a; 
     inside_step
diff --git a/diaframe_heap_lang/base_hints.v b/diaframe_heap_lang/base_hints.v
index 79ac03ba444f1304f56222bc5361102fe460845e..fbb5c420b0a8a750d26423d56b05b138dc825501 100644
--- a/diaframe_heap_lang/base_hints.v
+++ b/diaframe_heap_lang/base_hints.v
@@ -308,7 +308,7 @@ Section instances.
     Lemma array_from_shorter vs1 vs2 l l' q :
       SolveSepSideCondition (0 < length vs1 ≤ length vs2) →
       ComputeOffsetLoc l (length vs1) l' →
-      HINT l ↦∗{q} vs1 ✱ [- ; ⌜take (length vs1) vs2 = vs1⌝ ∗ l' ↦∗{q} (list.drop (length vs1) vs2) ] ⊫ [id];
+      HINT l ↦∗{q} vs1 ✱ [- ; ⌜take (length vs1) vs2 = vs1⌝ ∗ l' ↦∗{q} (drop (length vs1) vs2) ] ⊫ [id];
            l ↦∗{q} vs2 ✱ [emp].
     Proof.
       rewrite /SolveSepSideCondition => Hl <- /=.
diff --git a/supplements/coq-diaframe-actris.opam b/supplements/coq-diaframe-actris.opam
index e496587e5a79598b18b8f4c1a49495f25cce3a62..4865fca6db355c4f9274180c23fd51417bea0d35 100644
--- a/supplements/coq-diaframe-actris.opam
+++ b/supplements/coq-diaframe-actris.opam
@@ -10,7 +10,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/diaframe/-/issues"
 depends: [
   "coq-diaframe-heap-lang" {= version}
   "coq" { = "8.20.0" }
-  "coq-actris" { = "dev.2025-01-24.0.f9d06c7b" | = "~dev" }
+  "coq-actris" { = "dev.2025-03-28.0.c9249305" | = "~dev" }
 ]
 build: [make "-j%{jobs}%" "diaframe-actris"]
 install: [make "install-diaframe-actris"]
diff --git a/supplements/coq-diaframe-iris-examples.opam b/supplements/coq-diaframe-iris-examples.opam
index 7a49ba083986ee7de7622fe81ba5bd40ac318d57..b7ecde10f35e4b5bc5ddb07907e06ce43a6594a4 100644
--- a/supplements/coq-diaframe-iris-examples.opam
+++ b/supplements/coq-diaframe-iris-examples.opam
@@ -10,7 +10,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/diaframe/-/issues"
 depends: [
   "coq" { = "8.20.0" }
   "coq-diaframe-heap-lang" {= version}
-  "coq-iris-examples" { = "dev.2025-01-25.0.e5afd885" | = "~dev" }
+  "coq-iris-examples" { = "dev.2025-03-28.1.593cca1f" | = "~dev" }
 ]
 build: [make "-j%{jobs}%" "diaframe-iris-examples"]
 install: [make "install-diaframe-iris-examples"]
diff --git a/supplements/coq-diaframe-lambda-rust.opam b/supplements/coq-diaframe-lambda-rust.opam
index f050f1411a2e53a3c204cfdd4fa31a0cd0ad38e8..2bcecc1af3eb1e0aadcfa2be965fded6650cea3a 100644
--- a/supplements/coq-diaframe-lambda-rust.opam
+++ b/supplements/coq-diaframe-lambda-rust.opam
@@ -13,8 +13,8 @@ depends: [
   "coq-lambda-rust"
 ]
 pin-depends: [
-  ["coq-lambda-rust.dev" "git+https://gitlab.mpi-sws.org/iris/lambda-rust#f55b9243"]
-  ["coq-lifetime-logic.dev" "git+https://gitlab.mpi-sws.org/iris/lambda-rust#f55b9243"]
+  ["coq-lambda-rust.dev" "git+https://gitlab.mpi-sws.org/iris/lambda-rust#fca004c4"]
+  ["coq-lifetime-logic.dev" "git+https://gitlab.mpi-sws.org/iris/lambda-rust#fca004c4"]
 ]
 
 build: [make "-j%{jobs}%" "diaframe-lambda-rust"]
diff --git a/supplements/coq-diaframe-reloc.opam b/supplements/coq-diaframe-reloc.opam
index a694d94162e8565f84e546a982b3f5705572846d..fc060200b6a8234adf89ed1cdef52dea38b241a3 100644
--- a/supplements/coq-diaframe-reloc.opam
+++ b/supplements/coq-diaframe-reloc.opam
@@ -14,7 +14,7 @@ depends: [
   "coq-reloc"
 ]
 pin-depends: [
-  ["coq-reloc.dev" "git+https://gitlab.mpi-sws.org/iris/reloc#828ae710"]
+  ["coq-reloc.dev" "git+https://gitlab.mpi-sws.org/iris/reloc#37a694fd"]
 ]
 build: [make "-j%{jobs}%" "diaframe-reloc"]
 install: [make "install-diaframe-reloc"]
diff --git a/supplements/coq-diaframe-simuliris.opam b/supplements/coq-diaframe-simuliris.opam
index 3a5a2baf1921217a2cfb4dc125e1515e09ed8837..348eef9ae668f46057857410ca99b33499472bc8 100644
--- a/supplements/coq-diaframe-simuliris.opam
+++ b/supplements/coq-diaframe-simuliris.opam
@@ -13,7 +13,7 @@ depends: [
   "coq-simuliris"
 ]
 pin-depends: [
-  ["coq-simuliris.dev" "git+https://gitlab.mpi-sws.org/iris/simuliris#b7030e3a"]
+  ["coq-simuliris.dev" "git+https://gitlab.mpi-sws.org/iris/simuliris#771b052a"]
 ]
 build: [make "-j%{jobs}%" "diaframe-simuliris"]
 install: [make "install-diaframe-simuliris"]
diff --git a/supplements/diaframe_reloc/atomic_post_update.v b/supplements/diaframe_reloc/atomic_post_update.v
index 45bd1bf0bedc438c1b95b678a7bee74051ce2b09..feea205a61b5b5e342108bd9058bd185b4e1ab05 100644
--- a/supplements/diaframe_reloc/atomic_post_update.v
+++ b/supplements/diaframe_reloc/atomic_post_update.v
@@ -1,4 +1,5 @@
 From iris.bi Require Export bi telescopes lib.atomic.
+From iris.bi Require Import fixpoint_mono
 From iris.proofmode Require Import tactics notation reduction.
 From iris.program_logic Require Import weakestpre lifting atomic.
 From diaframe Require Import proofmode_base.
@@ -28,7 +29,7 @@ Section atomic_post_acc.
   Definition atomic_post_update_pre (Ψ : () → PROP) (_ : ()) : PROP :=
     atomic_post_acc Eo Ei Ef α (Ψ ()) β Φ.
 
-  Instance atomic_post_update_pre_mono : fixpoint.BiMonoPred atomic_post_update_pre.
+  Instance atomic_post_update_pre_mono : BiMonoPred atomic_post_update_pre.
   Proof.
     constructor.
     - iIntros (P1 P2 ??) "#HP12". iIntros ([]) "AU".
@@ -42,7 +43,7 @@ Section atomic_post_acc.
   Qed.
 
   Definition atomic_post_update_def :=
-    fixpoint.bi_greatest_fixpoint atomic_post_update_pre ().
+    bi_greatest_fixpoint atomic_post_update_pre ().
 End atomic_post_acc.
 
 (** Seal it *)
@@ -66,14 +67,14 @@ Section lemmas.
     rewrite atomic.atomic_update_unseal /atomic.atomic_update_def.
     rewrite atomic_post_update_eq /atomic_post_update_def.
     apply (anti_symm _).
-    - iApply (fixpoint.greatest_fixpoint_strong_mono with "[]").
+    - iApply (greatest_fixpoint_strong_mono with "[]").
       { apply atomic_update_pre_mono. }
       iIntros "!>" (F' []).
       rewrite /atomic_post_update_pre /atomic_update_pre.
       rewrite /atomic_acc /atomic_post_acc.
       iMod 1 as "[%x [Hα Hx]]".
       iExists _. by iFrame.
-    - iApply (fixpoint.greatest_fixpoint_strong_mono with "[]").
+    - iApply (greatest_fixpoint_strong_mono with "[]").
       { apply atomic_update_pre_mono. }
       iIntros "!>" (F' []).
       rewrite /atomic_post_update_pre /atomic_update_pre.
@@ -101,7 +102,7 @@ Section lemmas.
   Proof.
     rewrite atomic_post_update_eq /atomic_post_update_def.
     iIntros "HΦ #(Ha & Hf)".
-    iApply (fixpoint.greatest_fixpoint_strong_mono with "[] HΦ").
+    iApply (greatest_fixpoint_strong_mono with "[] HΦ").
     iIntros "!>" (F' []).
     rewrite /atomic_post_update_pre /atomic_post_acc.
     iMod 1 as "[%x [Hα Hx]]".
@@ -160,10 +161,10 @@ Section lemmas.
     move => Htrue P Q /=.
     iIntros "[>[$ H] HQ] !>".
     rewrite {2}atomic_post_update_eq /atomic_post_update_def.
-    iApply (fixpoint.greatest_fixpoint_coiter _ (λ _, _) with "[] [H HQ]"); last iAccu.
+    iApply (greatest_fixpoint_coiter _ (λ _, _) with "[] [H HQ]"); last iAccu.
     iIntros "!>" ([]) "[HAU HQ]".
     rewrite /atomic_post_update_pre /atomic_post_acc.
-    rewrite atomic_post_update_eq {1}/atomic_post_update_def fixpoint.greatest_fixpoint_unfold /atomic_post_update_pre /atomic_post_acc.
+    rewrite atomic_post_update_eq {1}/atomic_post_update_def greatest_fixpoint_unfold /atomic_post_update_pre /atomic_post_acc.
     iMod "HAU" as "[%x [HP Hr]]".
     iExists _. by iFrame.
   Qed.