diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index 13df9945d5cf943f53412f238ea5eada27139193..cce7437ae47b99a2192913bf088b8d50f8470615 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -94,10 +94,13 @@ Section bi_mixin.
     bi_mixin_wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R;
   }.
 
-  (** We equip any BI with a persistence modality that carves out the
-  intuitionistically fragment of the separation logic. For logics such as Iris,
+  (** We require any BI to have a persistence modality that carves out the
+  intuitionistic fragment of the separation logic. For logics such as Iris,
   the persistence modality has a non-trivial definition (involving the [core] of
-  the camera). However, for some simpler discrete BIs the persistence modality
+  the camera). It is not clear whether a trivial definition exists: while
+  [<pers> P := False] comes close, it does not satisfy [later_persistently_1].
+  
+  However, for some simpler discrete BIs the persistence modality
   can be defined as:
 
     <pers> P := ⌜ emp ⊢ P ⌝