diff --git a/CHANGELOG.md b/CHANGELOG.md
index f10c6edfdddacfcdcbdc445d776db40af233ba05..c4bd72c7a371683862efe5a10a6072b4082b0424 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -63,6 +63,8 @@ With this release, we dropped support for Coq 8.9.
   `big_sepL2_forall`, `big_sepMS_forall`, `big_sepMS_impl`, and `big_sepMS_dup`.
 * Remove `bi.tactics` with tactics that predate the proofmode (and that have not
   been working properly for quite some time).
+* Strengthen `persistent_sep_dup` to support propositions that are persistent
+  and either affine or absorbing.
 
 **Changes in `proofmode`:**
 
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 5227d08edd7f4512516cd7f93c08a9eb82bd9c4b..99a6783b752a99786230e770ced8e41b78d35f6f 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -729,13 +729,13 @@ Proof.
   rewrite -(absorbing emp) absorbingly_sep_l left_id //.
 Qed.
 
-Lemma sep_elim_l P Q `{H : TCOr (Affine Q) (Absorbing P)} : P ∗ Q ⊢ P.
+Lemma sep_elim_l P Q `{HQP : TCOr (Affine Q) (Absorbing P)} : P ∗ Q ⊢ P.
 Proof.
-  destruct H.
+  destruct HQP.
   - by rewrite (affine Q) right_id.
   - by rewrite (True_intro Q) comm.
 Qed.
-Lemma sep_elim_r P Q `{H : TCOr (Affine P) (Absorbing Q)} : P ∗ Q ⊢ Q.
+Lemma sep_elim_r P Q `{TCOr (Affine P) (Absorbing Q)} : P ∗ Q ⊢ Q.
 Proof. by rewrite comm sep_elim_l. Qed.
 
 Lemma sep_and P Q :
@@ -1365,8 +1365,16 @@ Proof.
   - by rewrite persistent_and_affinely_sep_r_1 affinely_elim.
 Qed.
 
-Lemma persistent_sep_dup P `{!Persistent P, !Absorbing P} : P ⊣⊢ P ∗ P.
-Proof. by rewrite -(persistent_persistently P) -persistently_sep_dup. Qed.
+Lemma persistent_sep_dup P
+    `{HP : !TCOr (Affine P) (Absorbing P), !Persistent P} :
+  P ⊣⊢ P ∗ P.
+Proof.
+  destruct HP; last by rewrite -(persistent_persistently P) -persistently_sep_dup.
+  apply (anti_symm (⊢)).
+  - by rewrite -{1}(intuitionistic_intuitionistically P)
+    intuitionistically_sep_dup intuitionistically_elim.
+  - by rewrite {1}(affine P) left_id.
+Qed.
 
 Lemma persistent_entails_l P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ Q ∗ P.
 Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
diff --git a/theories/bi/lib/fractional.v b/theories/bi/lib/fractional.v
index 04931d4c10fcea58363e1782fb7d97c4183939e4..ead88c5ca4ee8d4ada3008774de4f0b5706c01de 100644
--- a/theories/bi/lib/fractional.v
+++ b/theories/bi/lib/fractional.v
@@ -67,7 +67,7 @@ Section fractional.
   (** Fractional and logical connectives *)
   Global Instance persistent_fractional P :
     Persistent P → Absorbing P → Fractional (λ _, P).
-  Proof. intros ?? q q'. by apply bi.persistent_sep_dup. Qed.
+  Proof. intros ?? q q'. apply: bi.persistent_sep_dup. Qed.
 
   Global Instance fractional_sep Φ Ψ :
     Fractional Φ → Fractional Ψ → Fractional (λ q, Φ q ∗ Ψ q)%I.