diff --git a/CHANGELOG.md b/CHANGELOG.md
index 14f521a0cf506aff8a227cd04b9de4ed0f9423fe..8b03a559a8c7d22498db6cda45a327d1b76e82a0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -59,7 +59,9 @@ 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>`/`→`.
+* Improvements to `BiMonoPred`:
+  - Use `□`/`-∗` instead of `<pers>`/`→`.
+  - Strengthen to ensure that functions for recursive calls are non-expansive.
 
 **Changes in `proofmode`:**
 
diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index e4dd512cb7c076cb1a28e701fd66e7412c181d0e..13bfe0465e9261b32ae69613f4192af7482a2414 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -73,7 +73,7 @@ Section definition.
   Local Instance atomic_update_pre_mono : BiMonoPred atomic_update_pre.
   Proof.
     constructor.
-    - iIntros (P1 P2) "#HP12". iIntros ([]) "AU".
+    - iIntros (P1 P2 ??) "#HP12". iIntros ([]) "AU".
       iApply (make_laterable_intuitionistic_wand with "[] AU").
       iIntros "!> AA". iApply (atomic_acc_wand with "[HP12] AA").
       iSplit; last by eauto. iApply "HP12".
diff --git a/iris/bi/lib/fixpoint.v b/iris/bi/lib/fixpoint.v
index 32aafcc6fec935c9914329702c280ac510a358ba..45ca41fcb7d4c2562b58bf417e6f9a627bbb54ff 100644
--- a/iris/bi/lib/fixpoint.v
+++ b/iris/bi/lib/fixpoint.v
@@ -6,7 +6,10 @@ 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 Φ Ψ : □ (∀ x, Φ x -∗ Ψ x) -∗ ∀ x, F Φ x -∗ F Ψ x;
+  bi_mono_pred Φ Ψ :
+    NonExpansive Φ →
+    NonExpansive Ψ →
+    □ (∀ x, Φ x -∗ Ψ x) -∗ ∀ x, F Φ x -∗ F Ψ x;
   bi_mono_pred_ne Φ : NonExpansive Φ → NonExpansive (F Φ)
 }.
 Global Arguments bi_mono_pred {_ _ _ _} _ _.
@@ -37,7 +40,7 @@ Section least.
   Lemma least_fixpoint_unfold_2 x : F (bi_least_fixpoint F) x ⊢ bi_least_fixpoint F x.
   Proof using Type*.
     rewrite /bi_least_fixpoint /=. iIntros "HF" (Φ) "#Hincl".
-    iApply "Hincl". iApply (bi_mono_pred _ Φ with "[#]"); last done.
+    iApply "Hincl". iApply (bi_mono_pred _ Φ with "[#] HF"); [solve_proper|].
     iIntros "!>" (y) "Hy". iApply ("Hy" with "[# //]").
   Qed.
 
@@ -45,7 +48,7 @@ Section least.
     bi_least_fixpoint F x ⊢ F (bi_least_fixpoint F) x.
   Proof using Type*.
     iIntros "HF". iApply ("HF" $! (OfeMor (F (bi_least_fixpoint F))) with "[#]").
-    iIntros "!>" (y) "Hy /=". iApply (bi_mono_pred with "[#]"); last done.
+    iIntros "!>" (y) "Hy /=". iApply (bi_mono_pred with "[#] Hy").
     iIntros "!>" (z) "?". by iApply least_fixpoint_unfold_2.
   Qed.
 
@@ -68,7 +71,8 @@ Section least.
     trans (∀ x, bi_least_fixpoint F x -∗ Φ x ∧ bi_least_fixpoint F x)%I.
     { iIntros "#HΦ". iApply (least_fixpoint_ind with "[]"); first solve_proper.
       iIntros "!>" (y) "H". iSplit; first by iApply "HΦ".
-      iApply least_fixpoint_unfold_2. iApply (bi_mono_pred with "[#] H").
+      iApply least_fixpoint_unfold_2.
+      iApply (bi_mono_pred with "[#] H"); [solve_proper|].
       by iIntros "!> * [_ ?]". }
     by setoid_rewrite and_elim_l.
   Qed.
diff --git a/iris/bi/lib/relations.v b/iris/bi/lib/relations.v
index 9d7a3763505f108423fdffbdd7c1a8ade19a8008..a00a710d99c1511c002fa52fe3e6e4f0f4064b7e 100644
--- a/iris/bi/lib/relations.v
+++ b/iris/bi/lib/relations.v
@@ -17,7 +17,7 @@ Global Instance bi_rtc_pre_mono `{!BiInternalEq PROP}
   BiMonoPred (bi_rtc_pre R x).
 Proof.
   constructor; [|solve_proper].
-  iIntros (rec1 rec2) "#H". iIntros (x1) "[Hrec | Hrec]".
+  iIntros (rec1 rec2 ??) "#H". iIntros (x1) "[Hrec | Hrec]".
   { by iLeft. }
   iRight.
   iDestruct "Hrec" as (x') "[HP Hrec]".
diff --git a/iris/program_logic/total_adequacy.v b/iris/program_logic/total_adequacy.v
index 288e5138071feaabf52f99cc67418685b56d5e3c..3070bdc5d009dafecd01c0c7c96f0e581475d815 100644
--- a/iris/program_logic/total_adequacy.v
+++ b/iris/program_logic/total_adequacy.v
@@ -27,7 +27,7 @@ Qed.
 
 Local Instance twptp_pre_mono' : BiMonoPred twptp_pre.
 Proof.
-  constructor; first apply twptp_pre_mono.
+  constructor; first (intros ????; apply twptp_pre_mono).
   intros wp Hwp n t1 t2 ?%(discrete_iff _ _)%leibniz_equiv; solve_proper.
 Qed.
 
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index d6152e97b5860dcd758a74913e266bbd7553c387..3b8c9d06cb473f9984e3afd0b09f2be513e538a8 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -50,7 +50,7 @@ Definition twp_pre' `{!irisGS Λ Σ} (s : stuckness) :
 Local Instance twp_pre_mono' `{!irisGS Λ Σ} s : BiMonoPred (twp_pre' s).
 Proof.
   constructor.
-  - iIntros (wp1 wp2) "#H"; iIntros ([[E e1] Φ]); iRevert (E e1 Φ).
+  - iIntros (wp1 wp2 ??) "#H"; iIntros ([[E e1] Φ]); iRevert (E e1 Φ).
     iApply twp_pre_mono. iIntros "!>" (E e Φ). iApply ("H" $! (E,e,Φ)).
   - intros wp Hwp n [[E1 e1] Φ1] [[E2 e2] Φ2]
       [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=.