diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 8dac672cd2df049b2cf465385aff39facc32e030..33061f942250c53fa9ec21bc444586714c89dbea 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -110,8 +110,7 @@ Section bi_mixin.
     (* In the ordered RA model: `core` is idempotent *)
     bi_mixin_persistently_idemp_2 P : <pers> P ⊢ <pers> <pers> P;
 
-    (* In the ordered RA model: `core ε = ε`, which implies together with
-       monotonicity that `ε ≼ core x`. *)
+    (* In the ordered RA model: [ε ≼ core x]. *)
     bi_mixin_persistently_emp_intro P : P ⊢ <pers> emp;
 
     bi_mixin_persistently_forall_2 {A} (Ψ : A → PROP) :