diff --git a/CHANGELOG.md b/CHANGELOG.md
index d7c576cc6518d45494e6dd530d1b5f3c840f20f1..df598d46245d05a7a68b13e0221fe6f3d97c12b5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -59,6 +59,7 @@ Coq 8.11 is no longer supported in this version of Iris.
     As a consequence, `make_laterable_elim` got weaker: elimination now requires
     an except-0 modality (`make_laterable P -∗ ◇ P`).
   - Add `iModIntro` support for `make_laterable`.
+* State `bi_mono_pred` using `□`/`-∗` instead of `<pers>`/`→`.
 
 **Changes in `proofmode`:**
 
diff --git a/iris/bi/lib/fixpoint.v b/iris/bi/lib/fixpoint.v
index 52d8fb0ee9181a3dda696400d7a78ed75210a6af..9b242866f4c599721a4e99e9b5d3734a39174567 100644
--- a/iris/bi/lib/fixpoint.v
+++ b/iris/bi/lib/fixpoint.v
@@ -6,7 +6,7 @@ Import bi.
 (** Least and greatest fixpoint of a monotone function, defined entirely inside
     the logic.  *)
 Class BiMonoPred {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)) := {
-  bi_mono_pred Φ Ψ : ⊢ <pers> (∀ x, Φ x -∗ Ψ x) → ∀ x, F Φ x -∗ F Ψ x;
+  bi_mono_pred Φ Ψ : □ (∀ x, Φ x -∗ Ψ x) -∗ ∀ x, F Φ x -∗ F Ψ x;
   bi_mono_pred_ne Φ : NonExpansive Φ → NonExpansive (F Φ)
 }.
 Global Arguments bi_mono_pred {_ _ _ _} _ _.
diff --git a/iris/program_logic/total_adequacy.v b/iris/program_logic/total_adequacy.v
index ed100b2d8a091dead7ae550a27674bbd35a6489e..288e5138071feaabf52f99cc67418685b56d5e3c 100644
--- a/iris/program_logic/total_adequacy.v
+++ b/iris/program_logic/total_adequacy.v
@@ -16,8 +16,8 @@ Definition twptp_pre (twptp : list (expr Λ) → iProp Σ)
               ∃ nt', ⌜κ = []⌝ ∗ state_interp σ2 (S ns) κs nt' ∗ twptp t2.
 
 Lemma twptp_pre_mono (twptp1 twptp2 : list (expr Λ) → iProp Σ) :
-  ⊢ <pers> (∀ t, twptp1 t -∗ twptp2 t) →
-    ∀ t, twptp_pre twptp1 t -∗ twptp_pre twptp2 t.
+  □ (∀ t, twptp1 t -∗ twptp2 t) -∗
+  ∀ t, twptp_pre twptp1 t -∗ twptp_pre twptp2 t.
 Proof.
   iIntros "#H"; iIntros (t) "Hwp". rewrite /twptp_pre.
   iIntros (t2 σ1 ns κ κs σ2 nt1) "Hstep Hσ".