diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index d60d9a75eec8975d7ca5527f266c30b8c23c6bd6..a00d21347e2d10dee2b56da4dc867039f947dee2 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -742,6 +742,11 @@ Proof.
   apply persistently_mono, impl_elim with P; auto.
 Qed.
 
+Lemma persistently_emp_intro P : P ⊢ <pers> emp.
+Proof.
+  by rewrite -(left_id emp%I bi_sep P) {1}persistently_emp_2 persistently_absorbing.
+Qed.
+
 Lemma persistently_True_emp : <pers> True ⊣⊢ <pers> emp.
 Proof. apply (anti_symm _); auto using persistently_emp_intro. Qed.
 
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 33061f942250c53fa9ec21bc444586714c89dbea..21a05c617d314f21bdaf9bb2db7909feb8cd3c7d 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -111,7 +111,7 @@ Section bi_mixin.
     bi_mixin_persistently_idemp_2 P : <pers> P ⊢ <pers> <pers> P;
 
     (* In the ordered RA model: [ε ≼ core x]. *)
-    bi_mixin_persistently_emp_intro P : P ⊢ <pers> emp;
+    bi_mixin_persistently_emp_2 : emp ⊢ <pers> emp;
 
     bi_mixin_persistently_forall_2 {A} (Ψ : A → PROP) :
       (∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a);
@@ -394,8 +394,8 @@ Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed.
 Lemma persistently_idemp_2 P : <pers> P ⊢ <pers> <pers> P.
 Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed.
 
-Lemma persistently_emp_intro P : P ⊢ <pers> emp.
-Proof. eapply bi_mixin_persistently_emp_intro, bi_bi_mixin. Qed.
+Lemma persistently_emp_2 : (emp : PROP) ⊢ <pers> emp.
+Proof. eapply bi_mixin_persistently_emp_2, bi_bi_mixin. Qed.
 
 Lemma persistently_forall_2 {A} (Ψ : A → PROP) :
   (∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a).
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index c7fb6c7523829111ddb239000dd5ad38aef27449..d6ea57fc1191e226bacea245ade7e1e7d029f6dc 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -303,7 +303,7 @@ Proof.
     rewrite HP /= bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
   - intros P Q [?]. split=> i /=. by f_equiv.
   - intros P. split=> i. by apply bi.persistently_idemp_2.
-  - intros P. split=> i. by apply bi.persistently_emp_intro.
+  - split=> i. by apply bi.persistently_emp_intro.
   - intros A Ψ. split=> i. by apply bi.persistently_forall_2.
   - intros A Ψ. split=> i. by apply bi.persistently_exist_1.
   - intros P Q. split=> i. apply bi.sep_elim_l, _.