diff --git a/theories/bi/lib/fixpoint.v b/theories/bi/lib/fixpoint.v
index 975266f3f835835f35d8e8eaf9d9b5ce9288cdc8..0e4506f113a8fdff2e43c76ff144113772d726b8 100644
--- a/theories/bi/lib/fixpoint.v
+++ b/theories/bi/lib/fixpoint.v
@@ -45,7 +45,7 @@ Section least.
     bi_least_fixpoint F x ⊢ F (bi_least_fixpoint F) x.
   Proof.
     iIntros "HF". iApply ("HF" $! (CofeMor (F (bi_least_fixpoint F))) with "[#]").
-    iIntros "!#" (y) "Hy". iApply (bi_mono_pred with "[#]"); last done.
+    iIntros "!#" (y) "Hy /=". iApply (bi_mono_pred with "[#]"); last done.
     iIntros "!#" (z) "?". by iApply least_fixpoint_unfold_2.
   Qed.