diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 958d370623373b7d3b60c19a4981d21c81e5ed59..c683a11a74f73442789fca7307f5b408cd74442f 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -121,7 +121,7 @@ Section tests.
   Qed.
 
   Lemma test_iNext_Bi P :
-    @bi_entails monPredI (â–· P) (â–· P).
+    ▷ P ⊢@{monPredI} ▷ P.
   Proof. iIntros "H". by iNext. Qed.
 
   (** Test monPred_at framing *)