diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 4f2c323cfd688e58b14a85d8b51bd2dd7c1a51b3..9064ea39ccd434c929bcd17a53df612ef42d0572 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -1124,7 +1124,7 @@ Qed.
 
 Lemma affinely_persistently_sep_dup P : □ P ⊣⊢ □ P ∗ □ P.
 Proof.
-  by rewrite -persistently_and_affinely_sep_l affinely_and_r affinely_and idemp.
+  by rewrite -persistently_and_affinely_sep_l affinely_and_r idemp.
 Qed.
 
 Lemma impl_wand_affinely_persistently P Q : (bi_persistently P → Q) ⊣⊢ (□ P -∗ Q).
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index cf3780875ac4eeff67415fb4f7b1c87ea7cbd541..89d31c8c148217bf167317b4aa8d29deb361f7b4 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -48,9 +48,9 @@ Section bi_mixin.
   that combine both kinds of resources. In particular, we have an "ordered RA"
   model satisfying all these axioms. For this model, we extend RAs with an
   arbitrary partial order, and up-close resources wrt. that order (instead of
-  extension order).  We demand composition to be monotone wrt. the order.  We
-  define [emp := λ r, ε ≼ r]; persisently is still defined with the core: [□ P
-  := λ r, P (core r)].  *)
+  extension order).  We demand composition to be monotone wrt. the order: [x1 ≼
+  x2 → x1 ⋅ y ≼ x2 ⋅ y].  We define [emp := λ r, ε ≼ r]; persisently is still
+  defined with the core: [□ P := λ r, P (core r)].  *)
 
   Record BiMixin := {
     bi_mixin_entails_po : PreOrder bi_entails;
@@ -142,7 +142,7 @@ Section bi_mixin.
     (* In the ordered RA model: [x ≼ₑₓₜ y → core x ≼ core y] *)
     bi_mixin_persistently_absorbing P Q :
       bi_persistently P ∗ Q ⊢ bi_persistently P;
-    (* In the ordered RA model: [ε ≼ core x] *)
+    (* In the ordered RA model: [x ⋅ core x = core x], AND [ε ≼ core x]. *)
     bi_mixin_persistently_and_sep_elim P Q :
       bi_persistently P ∧ Q ⊢ (emp ∧ P) ∗ Q;
   }.