diff --git a/CHANGELOG.md b/CHANGELOG.md
index e2dfa3d07078000a5a140de34939177711f85a54..2fdd7bb0bd41b21ece34e6d1ab1982148e5be57a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -110,6 +110,12 @@ With this release, we dropped support for Coq 8.9.
 * Add an `mnat` library on top of `mnat_auth` that supports ghost state which is
   an authoritative, monotonically-increasing `nat` with a proposition giving a
   persistent lower bound. See `base_logic.lib.mnat` for further details.
+* Add a class, `Duplicable`, for duplicable propositions. The lemmas
+  `intuitionistically_sep_dup` and `plainly_sep_duplicable` are now instances. A
+  few lemmas are changed to use the new class: `inv_combine_dup_l`,
+  `big_sepL_dup`, `big_sepM_dup`, `big_sepS_dup`. Instead of having `□ (P -∗ P ∗
+  P)` as an assumption these lemmas now assume `P` to be an instance of
+  `Duplicable`.
 
 **Changes in `program_logic`:**
 
@@ -133,6 +139,7 @@ s/\bauth_both_frac_valid\b/auth_both_frac_valid_discrete/g
 # gen_heap_ctx and proph_map_ctx
 s/\bgen_heap_ctx\b/gen_heap_interp/g
 s/\bproph_map_ctx\b/proph_map_interp/g
+s/\bintuitionistically_sep_dup\b/(duplicable (â–¡ _))/g
 EOF
 ```
 
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index b3f0cee87069a59a0f5b64e50a8e2832f1854a85..313d54aa38e3e05c8d8281cd12f7ab063a8f70e0 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -77,6 +77,8 @@ Global Instance ownM_persistent a : CoreId a → Persistent (@uPred_ownM M a).
 Proof.
   intros. rewrite /Persistent -{2}(core_id_core a). apply persistently_ownM_core.
 Qed.
+Global Instance ownM_duplicable a : CoreId a → Duplicable (@uPred_ownM M a).
+Proof. intros. apply: persistent_sep_duplicable. Qed.
 
 (** For big ops *)
 Global Instance uPred_ownM_sep_homomorphism :
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index d02ce530697f2199d52f6c924a832f6468d87a84..d6f93ba166f4672a9e5f5f69945c3280eb2c24c0 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -33,6 +33,8 @@ Section definitions.
   Proof. apply _. Qed.
   Global Instance auth_own_core_id a : CoreId a → Persistent (auth_own a).
   Proof. apply _. Qed.
+  Global Instance auth_own_core_id_duplicable a : CoreId a → Duplicable (auth_own a).
+  Proof. apply _. Qed.
 
   Global Instance auth_inv_ne n :
     Proper (pointwise_relation T (dist n) ==>
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index adff4f6eb0a06733e346c854757bbc8bc6f9323a..76f570e234b2a430869bab2fee6d0e3da195abd1 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -97,6 +97,9 @@ Section inv.
   Global Instance inv_persistent N P : Persistent (inv N P).
   Proof. rewrite inv_eq. apply _. Qed.
 
+  Global Instance inv_duplicable N P : Duplicable (inv N P).
+  Proof. rewrite inv_eq. apply _. Qed.
+
   Lemma inv_alter N P Q : inv N P -∗ ▷ □ (P -∗ Q ∗ (Q -∗ P)) -∗ inv N Q.
   Proof.
     rewrite inv_eq. iIntros "#HI #HPQ !>" (E H).
@@ -145,13 +148,12 @@ Section inv.
     iMod "Hclose" as %_. iMod ("HcloseQ" with "HQ") as %_. by iApply "HcloseP".
   Qed.
 
-  Lemma inv_combine_dup_l N P Q :
-    □ (P -∗ P ∗ P) -∗
+  Lemma inv_combine_dup_l P `{!Duplicable P} N Q :
     inv N P -∗ inv N Q -∗ inv N (P ∗ Q).
   Proof.
-    rewrite inv_eq. iIntros "#HPdup #HinvP #HinvQ !>" (E ?).
+    rewrite inv_eq. iIntros "#HinvP #HinvQ !>" (E ?).
     iMod ("HinvP" with "[//]") as "[HP HcloseP]".
-    iDestruct ("HPdup" with "HP") as "[$ HP]".
+    iDestruct (duplicable P with "HP") as "[$ HP]".
     iMod ("HcloseP" with "HP") as %_.
     iMod ("HinvQ" with "[//]") as "[$ HcloseQ]".
     iIntros "!> [HP HQ]". by iApply "HcloseQ".
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 66684fb4d093b24c50a4faebf70fe4b73ce11001..f522aa8f132417fe11f71b75260cfa31ccc8a858 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -193,6 +193,8 @@ Global Instance own_timeless γ a : Discrete a → Timeless (own γ a).
 Proof. rewrite !own_eq /own_def. apply _. Qed.
 Global Instance own_core_persistent γ a : CoreId a → Persistent (own γ a).
 Proof. rewrite !own_eq /own_def; apply _. Qed.
+Global Instance own_core_duplicable γ a : CoreId a → Duplicable (own γ a).
+Proof. rewrite !own_eq /own_def; apply _. Qed.
 
 Lemma later_own γ a : ▷ own γ a -∗ ◇ ∃ b, own γ b ∧ ▷ (a ≡ b).
 Proof.
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index ea7b86b0d1b97add8dbf4e2e4327ffe3f72f51d1..f40575296c48f42bb81ffa051e6e86ffca89f1e8 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -201,7 +201,7 @@ Section sep_list.
   Proof.
     apply wand_intro_l. revert Φ Ψ. induction l as [|x l IH]=> Φ Ψ /=.
     { by rewrite sep_elim_r. }
-    rewrite intuitionistically_sep_dup -assoc [(□ _ ∗ _)%I]comm -!assoc assoc.
+    rewrite (duplicable (□ _)) -assoc [(□ _ ∗ _)%I]comm -!assoc assoc.
     apply sep_mono.
     - rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
       by rewrite intuitionistically_elim wand_elim_l.
@@ -210,13 +210,11 @@ Section sep_list.
       apply forall_intro=> k. by rewrite (forall_elim (S k)).
   Qed.
 
-  Lemma big_sepL_dup P `{!Affine P} l :
-    □ (P -∗ P ∗ P) -∗ P -∗ [∗ list] k↦x ∈ l, P.
+  Lemma big_sepL_dup P `{!Affine P, !Duplicable P} l :
+    P -∗ [∗ list] k↦x ∈ l, P.
   Proof.
-    apply wand_intro_l.
     induction l as [|x l IH]=> /=; first by apply: affine.
-    rewrite intuitionistically_sep_dup {1}intuitionistically_elim.
-    rewrite assoc wand_elim_r -assoc. apply sep_mono; done.
+    rewrite {1}(duplicable P). apply sep_mono; done.
   Qed.
 
   Lemma big_sepL_delete Φ l i x :
@@ -269,6 +267,16 @@ Section sep_list.
     TCForall Persistent Ps → Persistent ([∗] Ps).
   Proof. induction 1; simpl; apply _. Qed.
 
+  Global Instance big_sepL_nil_duplicable Φ :
+    Duplicable ([∗ list] k↦x ∈ [], Φ k x).
+  Proof. simpl; apply _. Qed.
+  Global Instance big_sepL_duplicable Φ l :
+    (∀ k x, Duplicable (Φ k x)) → Duplicable ([∗ list] k↦x ∈ l, Φ k x).
+  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+  Global Instance big_sepL_duplicable_id Ps :
+    TCForall Duplicable Ps → Duplicable ([∗] Ps).
+  Proof. induction 1; simpl; apply _. Qed.
+
   Global Instance big_sepL_nil_affine Φ :
     Affine ([∗ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.
@@ -557,7 +565,7 @@ Section sep_list2.
   Proof.
     apply wand_intro_l. revert Φ Ψ l2.
     induction l1 as [|x1 l1 IH]=> Φ Ψ [|x2 l2] /=; [by rewrite sep_elim_r..|].
-    rewrite intuitionistically_sep_dup -assoc [(□ _ ∗ _)%I]comm -!assoc assoc.
+    rewrite (duplicable (□ _)) -assoc [(□ _ ∗ _)%I]comm -!assoc assoc.
     apply sep_mono.
     - rewrite (forall_elim 0) (forall_elim x1) (forall_elim x2) !pure_True // !True_impl.
       by rewrite intuitionistically_elim wand_elim_l.
@@ -602,6 +610,14 @@ Section sep_list2.
     Persistent ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
   Proof. rewrite big_sepL2_alt. apply _. Qed.
 
+  Global Instance big_sepL2_nil_duplicable Φ :
+    Duplicable ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2).
+  Proof. simpl; apply _. Qed.
+  Global Instance big_sepL2_duplicable Φ l1 l2 :
+    (∀ k x1 x2, Duplicable (Φ k x1 x2)) →
+    Duplicable ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2).
+  Proof. intros. rewrite big_sepL2_alt. apply: duplicable_and_persistent_l. Qed.
+
   Global Instance big_sepL2_nil_affine Φ :
     Affine ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2).
   Proof. simpl; apply _. Qed.
@@ -734,6 +750,10 @@ Section and_list.
   Global Instance big_andL_persistent Φ l :
     (∀ k x, Persistent (Φ k x)) → Persistent ([∧ list] k↦x ∈ l, Φ k x).
   Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+
+  Global Instance big_andL_nil_duplicable Φ :
+    Duplicable ([∧ list] k↦x ∈ [], Φ k x).
+  Proof. simpl; apply _. Qed.
 End and_list.
 
 Section or_list.
@@ -845,6 +865,13 @@ Section or_list.
   Global Instance big_orL_persistent Φ l :
     (∀ k x, Persistent (Φ k x)) → Persistent ([∨ list] k↦x ∈ l, Φ k x).
   Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+
+  Global Instance big_orL_nil_duplicable Φ :
+    Duplicable ([∨ list] k↦x ∈ [], Φ k x).
+  Proof. simpl; apply _. Qed.
+  Global Instance big_orL_duplicable `{BiAffine PROP} Φ l :
+    (∀ k x, Duplicable (Φ k x)) → Duplicable ([∨ list] k↦x ∈ l, Φ k x).
+  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
 End or_list.
 
 (** ** Big ops over finite maps *)
@@ -1028,7 +1055,7 @@ Section map.
   Proof.
     apply wand_intro_l. induction m as [|i x m ? IH] using map_ind.
     { by rewrite big_opM_eq sep_elim_r. }
-    rewrite !big_sepM_insert // intuitionistically_sep_dup.
+    rewrite !big_sepM_insert // (duplicable (â–¡ _)).
     rewrite -assoc [(□ _ ∗ _)%I]comm -!assoc assoc. apply sep_mono.
     - rewrite (forall_elim i) (forall_elim x) pure_True ?lookup_insert //.
       by rewrite True_impl intuitionistically_elim wand_elim_l.
@@ -1039,14 +1066,12 @@ Section map.
       by rewrite pure_True // True_impl.
   Qed.
 
-  Lemma big_sepM_dup P `{!Affine P} m :
-    □ (P -∗ P ∗ P) -∗ P -∗ [∗ map] k↦x ∈ m, P.
+  Lemma big_sepM_dup P `{!Affine P, !Duplicable P} m :
+    P -∗ [∗ map] k↦x ∈ m, P.
   Proof.
-    apply wand_intro_l. induction m as [|i x m ? IH] using map_ind.
-    { apply: big_sepM_empty'. }
-    rewrite !big_sepM_insert //.
-    rewrite intuitionistically_sep_dup {1}intuitionistically_elim.
-    rewrite assoc wand_elim_r -assoc. apply sep_mono; done.
+    induction m as [|i x m ? IH] using map_ind.
+    - apply: big_sepM_empty'.
+    - rewrite !big_sepM_insert // {1}(duplicable P). apply sep_mono; done.
   Qed.
 
   Lemma big_sepM_later `{BiAffine PROP} Φ m :
@@ -1070,6 +1095,13 @@ Section map.
     (∀ k x, Persistent (Φ k x)) → Persistent ([∗ map] k↦x ∈ m, Φ k x).
   Proof. rewrite big_opM_eq. intros. apply big_sepL_persistent=> _ [??]; apply _. Qed.
 
+  Global Instance big_sepM_empty_duplicable Φ :
+    Duplicable ([∗ map] k↦x ∈ ∅, Φ k x).
+  Proof. rewrite big_opM_eq /big_opM_def map_to_list_empty. apply _. Qed.
+  Global Instance big_sepM_duplicable Φ m :
+    (∀ k x, Duplicable (Φ k x)) → Duplicable ([∗ map] k↦x ∈ m, Φ k x).
+  Proof. rewrite big_opM_eq. intros. apply big_sepL_duplicable=> _ [??]; apply _. Qed.
+
   Global Instance big_sepM_empty_affine Φ :
     Affine ([∗ map] k↦x ∈ ∅, Φ k x).
   Proof. rewrite big_opM_eq /big_opM_def map_to_list_empty. apply _. Qed.
@@ -1452,6 +1484,14 @@ Section map2.
     Persistent ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2).
   Proof. rewrite big_sepM2_eq /big_sepM2_def. apply _. Qed.
 
+  Global Instance big_sepM2_empty_duplicable Φ :
+    Duplicable ([∗ map] k↦y1;y2 ∈ ∅; ∅, Φ k y1 y2).
+  Proof. rewrite big_sepM2_empty. apply _. Qed.
+  Global Instance big_sepM2_duplicable Φ m1 m2 :
+    (∀ k x1 x2, Duplicable (Φ k x1 x2)) →
+    Duplicable ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2).
+  Proof. intros. rewrite big_sepM2_eq /big_sepM2_def. apply: duplicable_and_persistent_l. Qed.
+
   Global Instance big_sepM2_empty_affine Φ :
     Affine ([∗ map] k↦y1;y2 ∈ ∅; ∅, Φ k y1 y2).
   Proof. rewrite big_sepM2_empty. apply _. Qed.
@@ -1633,7 +1673,7 @@ Section gset.
   Proof.
     apply wand_intro_l. induction X as [|x X ? IH] using set_ind_L.
     { by rewrite big_opS_eq sep_elim_r. }
-    rewrite !big_sepS_insert // intuitionistically_sep_dup.
+    rewrite !big_sepS_insert // (duplicable (â–¡ _)).
     rewrite -assoc [(□ _ ∗ _)%I]comm -!assoc assoc. apply sep_mono.
     - rewrite (forall_elim x) pure_True; last set_solver.
       by rewrite True_impl intuitionistically_elim wand_elim_l.
@@ -1642,14 +1682,11 @@ Section gset.
       by rewrite pure_True ?True_impl; last set_solver.
   Qed.
 
-  Lemma big_sepS_dup P `{!Affine P} X :
-    □ (P -∗ P ∗ P) -∗ P -∗ [∗ set] x ∈ X, P.
+  Lemma big_sepS_dup P `{!Affine P, !Duplicable P} X : P -∗ [∗ set] x ∈ X, P.
   Proof.
-    apply wand_intro_l. induction X as [|x X ? IH] using set_ind_L.
-    { apply: big_sepS_empty'. }
-    rewrite !big_sepS_insert //.
-    rewrite intuitionistically_sep_dup {1}intuitionistically_elim.
-    rewrite assoc wand_elim_r -assoc. apply sep_mono; done.
+    induction X as [|x X ? IH] using set_ind_L.
+    - apply: big_sepS_empty'.
+    - rewrite !big_sepS_insert // {1}(duplicable P). apply sep_mono; done.
   Qed.
 
   Lemma big_sepS_later `{BiAffine PROP} Φ X :
@@ -1673,6 +1710,13 @@ Section gset.
     (∀ x, Persistent (Φ x)) → Persistent ([∗ set] x ∈ X, Φ x).
   Proof. rewrite big_opS_eq /big_opS_def. apply _. Qed.
 
+  Global Instance big_sepS_empty_duplicable Φ :
+    Duplicable ([∗ set] x ∈ ∅, Φ x).
+  Proof. rewrite big_opS_eq /big_opS_def elements_empty. apply _. Qed.
+  Global Instance big_sepS_duplicable Φ X :
+    (∀ x, Duplicable (Φ x)) → Duplicable ([∗ set] x ∈ X, Φ x).
+  Proof. rewrite big_opS_eq /big_opS_def. apply _. Qed.
+
   Global Instance big_sepS_empty_affine Φ : Affine ([∗ set] x ∈ ∅, Φ x).
   Proof. rewrite big_opS_eq /big_opS_def elements_empty. apply _. Qed.
   Global Instance big_sepS_affine Φ X :
@@ -1785,6 +1829,13 @@ Section gmultiset.
     (∀ x, Persistent (Φ x)) → Persistent ([∗ mset] x ∈ X, Φ x).
   Proof. rewrite big_opMS_eq /big_opMS_def. apply _. Qed.
 
+  Global Instance big_sepMS_empty_duplicable Φ :
+    Duplicable ([∗ mset] x ∈ ∅, Φ x).
+  Proof. rewrite big_opMS_eq /big_opMS_def gmultiset_elements_empty. apply _. Qed.
+  Global Instance big_sepMS_duplicable Φ X :
+    (∀ x, Duplicable (Φ x)) → Duplicable ([∗ mset] x ∈ X, Φ x).
+  Proof. rewrite big_opMS_eq /big_opMS_def. apply _. Qed.
+
   Global Instance big_sepMS_empty_affine Φ : Affine ([∗ mset] x ∈ ∅, Φ x).
   Proof. rewrite big_opMS_eq /big_opMS_def gmultiset_elements_empty. apply _. Qed.
   Global Instance big_sepMS_affine Φ X :
diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index fdeb3a982771514003b786b90575c8b3ae70b39d..40da60d3a1686cdcd7ddfb7bcfbd2c1eeeac155b 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -19,6 +19,12 @@ Arguments persistent {_} _%I {_}.
 Hint Mode Persistent + ! : typeclass_instances.
 Instance: Params (@Persistent) 1 := {}.
 
+Class Duplicable {PROP : bi} (P : PROP) := duplicable : P ⊢ P ∗ P.
+Arguments Duplicable {_} _%I : simpl never.
+Arguments duplicable {_} _%I {_}.
+Hint Mode Duplicable + ! : typeclass_instances.
+Instance: Params (@Duplicable) 1 := {}.
+
 Definition bi_affinely {PROP : bi} (P : PROP) : PROP := (emp ∧ P)%I.
 Arguments bi_affinely {_} _%I : simpl never.
 Instance: Params (@bi_affinely) 1 := {}.
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index b8170151aca1b3a9cff8f70f0c7696db4d8f36fb..c9f819ede0d737e4484f269e569ca07a310432f0 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -443,7 +443,7 @@ Proof.
     by rewrite -(exist_intro a).
   - apply exist_elim=> a; apply sep_mono; auto using exist_intro.
 Qed.
-Lemma sep_exist_r {A} (Φ: A → PROP) Q: (∃ a, Φ a) ∗ Q ⊣⊢ ∃ a, Φ a ∗ Q.
+Lemma sep_exist_r {A} (Φ : A → PROP) Q: (∃ a, Φ a) ∗ Q ⊣⊢ ∃ a, Φ a ∗ Q.
 Proof. setoid_rewrite (comm _ _ Q); apply sep_exist_l. Qed.
 Lemma sep_forall_l {A} P (Ψ : A → PROP) : P ∗ (∀ a, Ψ a) ⊢ ∀ a, P ∗ Ψ a.
 Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
@@ -900,13 +900,10 @@ Proof.
   rewrite persistently_forall_2. auto using persistently_mono, pure_intro.
 Qed.
 
-Lemma persistently_sep_dup P : <pers> P ⊣⊢ <pers> P ∗ <pers> P.
+Global Instance persistently_sep_duplicable P : Duplicable (<pers> P).
 Proof.
-  apply (anti_symm _).
-  - rewrite -{1}(idemp bi_and (<pers> _)%I).
-    by rewrite -{2}(emp_sep (<pers> _)%I)
-      persistently_and_sep_assoc and_elim_l.
-  - by rewrite persistently_absorbing.
+  rewrite /Duplicable -{1}(idemp bi_and (<pers> _)%I).
+  by rewrite -{2}(emp_sep (<pers> _)%I) persistently_and_sep_assoc and_elim_l.
 Qed.
 
 Lemma persistently_and_sep_l_1 P Q : <pers> P ∧ Q ⊢ <pers> P ∗ Q.
@@ -1103,9 +1100,10 @@ Proof.
   by rewrite -persistently_and_intuitionistically_sep_l -affinely_and affinely_and_r.
 Qed.
 
-Lemma intuitionistically_sep_dup P : □ P ⊣⊢ □ P ∗ □ P.
+Global Instance intuitionistically_sep_duplicable P : Duplicable (â–¡ P).
 Proof.
-  by rewrite -persistently_and_intuitionistically_sep_l affinely_and_r idemp.
+  by rewrite /Duplicable -persistently_and_intuitionistically_sep_l
+    affinely_and_r idemp.
 Qed.
 
 Lemma impl_wand_intuitionistically P Q : (<pers> P → Q) ⊣⊢ (□ P -∗ Q).
@@ -1115,12 +1113,11 @@ Proof.
   - apply impl_intro_l. by rewrite persistently_and_intuitionistically_sep_l wand_elim_r.
 Qed.
 
-Lemma intuitionistically_alt_fixpoint P :
-  □ P ⊣⊢ emp ∧ (P ∗ □ P).
+Lemma intuitionistically_alt_fixpoint P : □ P ⊣⊢ emp ∧ (P ∗ □ P).
 Proof.
   apply (anti_symm (⊢)).
   - apply and_intro; first exact: affinely_elim_emp.
-    rewrite {1}intuitionistically_sep_dup. apply sep_mono; last done.
+    rewrite {1}(duplicable (â–¡ _)). apply sep_mono; last done.
     apply intuitionistically_elim.
   - apply and_mono; first done. rewrite /bi_intuitionistically {2}persistently_alt_fixpoint.
     apply sep_mono; first done. apply and_elim_r.
@@ -1365,8 +1362,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.
+(* Not an instance, see the bottom of this file *)
+Lemma persistent_sep_duplicable P
+  `{HP : !TCOr (Affine P) (Absorbing P), !Persistent P} :
+  Duplicable P.
+Proof.
+  rewrite /Duplicable. destruct HP.
+  - by rewrite -{1}(intuitionistic_intuitionistically P)
+      intuitionistically_sep_duplicable intuitionistically_elim.
+  - rewrite -(persistent_persistently P). apply: duplicable.
+Qed.
 
 Lemma persistent_entails_l P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ Q ∗ P.
 Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
@@ -1533,6 +1538,58 @@ Global Instance from_option_persistent {A} P (Ψ : A → PROP) (mx : option A) :
   (∀ x, Persistent (Ψ x)) → Persistent P → Persistent (from_option Ψ P mx).
 Proof. destruct mx; apply _. Qed.
 
+Lemma duplicable_equiv P `{!Duplicable P, !TCOr (Affine P) (Absorbing P)} :
+  P ⊣⊢ P ∗ P.
+Proof. apply (anti_symm _); [done|apply: sep_elim_l]. Qed.
+
+(* Duplicable instances *)
+Global Instance Duplicable_proper : Proper ((⊣⊢) ==> iff) (@Duplicable PROP).
+Proof. solve_proper. Qed.
+
+Global Instance pure_duplicable φ : Duplicable (PROP:=PROP) ⌜φ⌝.
+Proof. rewrite /Duplicable -persistently_pure. apply (duplicable (<pers> _)). Qed.
+Global Instance emp_duplicable : Duplicable (PROP:=PROP) emp.
+Proof. by rewrite /Duplicable left_id. Qed.
+
+Global Instance exist_duplicable {A} (Ψ : A → PROP) :
+  (∀ x, Duplicable (Ψ x)) → Duplicable (∃ x, Ψ x).
+Proof.
+  rewrite /Duplicable. intros Hp.
+  apply exist_elim=> a. rewrite (Hp a). apply sep_mono; apply exist_intro.
+Qed.
+Global Instance or_duplicable P Q :
+  Duplicable P → Duplicable Q → Duplicable (P ∨ Q).
+Proof. intros. rewrite or_alt. apply exist_duplicable. intros [|]; done. Qed.
+
+Global Instance sep_duplicable P Q :
+  Duplicable P → Duplicable Q → Duplicable (P ∗ Q).
+Proof.
+  intros. rewrite /Duplicable assoc (comm _ _ P) assoc -(duplicable P).
+  by rewrite -assoc -(duplicable Q).
+Qed.
+
+Lemma duplicable_and_persistent_l P Q :
+  Persistent P → Absorbing P → Duplicable Q → Duplicable (P ∧ Q).
+Proof.
+  intros. rewrite /Duplicable.
+  rewrite -persistent_and_sep_assoc (comm _ Q) -persistent_and_sep_assoc -duplicable.
+  auto.
+Qed.
+
+Lemma duplicable_and_persistent_r P Q :
+  Persistent Q → Absorbing Q → Duplicable P → Duplicable (P ∧ Q).
+Proof. rewrite comm. apply duplicable_and_persistent_l. Qed.
+
+Global Instance persistently_duplicable P : Duplicable (<pers> P).
+Proof. apply: persistent_sep_duplicable. Qed.
+Global Instance absorbingly_duplicable P : Duplicable P → Duplicable (<absorb> P).
+Proof. rewrite /bi_absorbingly. apply _. Qed.
+Global Instance absorbingly_if_duplicable p P : Duplicable P → Duplicable (<absorb>?p P).
+Proof. destruct p; simpl; apply _. Qed.
+Global Instance from_option_duplicable {A} P (Ψ : A → PROP) (mx : option A) :
+  (∀ x, Duplicable (Ψ x)) → Duplicable P → Duplicable (from_option Ψ P mx).
+Proof. destruct mx; apply _. Qed.
+
 (* For big ops *)
 Global Instance bi_and_monoid : Monoid (@bi_and PROP) :=
   {| monoid_unit := True%I |}.
@@ -1587,4 +1644,15 @@ Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A → PROP)
   NonExpansive Φ → LimitPreserving (λ x, Persistent (Φ x)).
 Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
 End derived.
+
+(* When declared as an actual instance, [persistent_sep_duplicable] will cause
+failing proof searches to take exponential time, as Coq will try to
+apply it the instance at any node in the proof search tree.
+
+To avoid that, we declare it using a [Hint Immediate], so that it will
+only be used at the leaves of the proof search tree, i.e. when the
+premise of the hint can be derived from just the current context. *)
+(* FIXME: This hint does not work due to the [TCOr] in [persistent_sep_duplicable]. *)
+Hint Immediate persistent_sep_duplicable : typeclass_instances.
+
 End bi.
diff --git a/theories/bi/derived_laws_later.v b/theories/bi/derived_laws_later.v
index a683467de724d154d0e9fc20e20c22eba4df1cec..7c52a63516887cfbc485fe4f58fe6f5eb0a173db 100644
--- a/theories/bi/derived_laws_later.v
+++ b/theories/bi/derived_laws_later.v
@@ -271,7 +271,7 @@ Lemma except_0_sep P Q : ◇ (P ∗ Q) ⊣⊢ ◇ P ∗ ◇ Q.
 Proof.
   rewrite /bi_except_0. apply (anti_symm _).
   - apply or_elim; last by auto using sep_mono.
-    by rewrite -!or_intro_l -persistently_pure -later_sep -persistently_sep_dup.
+    by rewrite -!or_intro_l -persistently_pure -later_sep -duplicable.
   - rewrite sep_or_r !sep_or_l {1}(later_intro P) {1}(later_intro Q).
     rewrite -!later_sep !left_absorb right_absorb. auto.
 Qed.
diff --git a/theories/bi/internal_eq.v b/theories/bi/internal_eq.v
index 3ffb1d71f4332e5eba60fdfde98813cf1226f948..736b6669fcf6631b8c2b54a3d000ccb8dc521679 100644
--- a/theories/bi/internal_eq.v
+++ b/theories/bi/internal_eq.v
@@ -219,6 +219,9 @@ Proof. by rewrite /Absorbing absorbingly_internal_eq. Qed.
 Global Instance internal_eq_persistent {A : ofeT} (a b : A) :
   Persistent (PROP:=PROP) (a ≡ b).
 Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.
+Global Instance internal_eq_duplicable {A : ofeT} (a b : A) :
+  Duplicable (PROP:=PROP) (a ≡ b).
+Proof. apply: persistent_sep_duplicable. Qed.
 
 (* Equality under a later. *)
 Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A → PROP)
diff --git a/theories/bi/lib/fractional.v b/theories/bi/lib/fractional.v
index 04931d4c10fcea58363e1782fb7d97c4183939e4..6888a5f6a6cb261aaec514bc5109a2fafa60b99c 100644
--- a/theories/bi/lib/fractional.v
+++ b/theories/bi/lib/fractional.v
@@ -63,11 +63,24 @@ Section fractional.
     AsFractional P Φ q → AsFractional P12 Φ (q/2) →
     P12 -∗ P12 -∗ P.
   Proof. intros. apply bi.wand_intro_r. by rewrite -(fractional_half P). Qed.
+  
+  Lemma fractional_duplicable `{!Fractional Φ} : Duplicable (∃ q, Φ q).
+  Proof.
+    rewrite /Duplicable.
+    apply bi.exist_elim=> q. rewrite -(Qp_div_2 q) {1}fractional.
+    apply bi.sep_mono; apply bi.exist_intro.
+  Qed.
 
   (** 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.
+    (* FIXME: The hint for [persistent_sep_duplicable] should apply here. *)
+    intros ? ? q q'. apply: bi.duplicable_equiv. apply: bi.persistent_sep_duplicable.
+  Qed.
+  Global Instance duplicable_fractional P :
+    Duplicable P → Absorbing P → Fractional (λ _, P).
+  Proof. intros ? ? q q'. apply: bi.duplicable_equiv. Qed.
 
   Global Instance fractional_sep Φ Ψ :
     Fractional Φ → Fractional Ψ → Fractional (λ q, Φ q ∗ Ψ q)%I.
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index 756dba593fd955d1b4067b4da66f758d15af765c..c977d532f3310d0ac29ae6584c80a6a2192dcea8 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -199,12 +199,10 @@ Qed.
 Lemma plainly_emp_2 : emp ⊢@{PROP} ■ emp.
 Proof. apply plainly_emp_intro. Qed.
 
-Lemma plainly_sep_dup P : ■ P ⊣⊢ ■ P ∗ ■ P.
+Global Instance plainly_sep_duplicable P : Duplicable (â–  P).
 Proof.
-  apply (anti_symm _).
-  - rewrite -{1}(idemp bi_and (â–  _)%I).
-    by rewrite -{2}(emp_sep (â–  _)%I) plainly_and_sep_assoc and_elim_l.
-  - by rewrite plainly_absorb.
+  rewrite /Duplicable. rewrite -{1}(idemp bi_and (â–  _)%I).
+  by rewrite -{2}(emp_sep (â–  _)%I) plainly_and_sep_assoc and_elim_l.
 Qed.
 
 Lemma plainly_and_sep_l_1 P Q : ■ P ∧ Q ⊢ ■ P ∗ Q.
diff --git a/theories/bi/telescopes.v b/theories/bi/telescopes.v
index 2bef8b0e78e131b20140a3b57642ac86d031419f..ea989e6fa92446009267f6d7b1a05036246e68cb 100644
--- a/theories/bi/telescopes.v
+++ b/theories/bi/telescopes.v
@@ -84,6 +84,9 @@ Section telescopes.
   Global Instance bi_texist_persistent Ψ :
     (∀ x, Persistent (Ψ x)) → Persistent (∃.. x, Ψ x).
   Proof. rewrite bi_texist_exist. apply _. Qed.
+  Global Instance bi_texist_duplicable Ψ :
+    (∀ x, Duplicable (Ψ x)) → Duplicable (∃.. x, Ψ x).
+  Proof. rewrite bi_texist_exist. apply _. Qed.
 
   Global Instance bi_tforall_timeless Ψ :
     (∀ x, Timeless (Ψ x)) → Timeless (∀.. x, Ψ x).
diff --git a/theories/proofmode/class_instances_later.v b/theories/proofmode/class_instances_later.v
index ffab7068c7775a9012011705441a422f8b652f5c..77baee77f0a21d23ec77a299a75d586be2896908 100644
--- a/theories/proofmode/class_instances_later.v
+++ b/theories/proofmode/class_instances_later.v
@@ -77,6 +77,14 @@ Global Instance from_sep_except_0 P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (◇ P) (◇ Q1) (◇ Q2).
 Proof. rewrite /FromSep=><-. by rewrite except_0_sep. Qed.
 
+(* Duplicable *)
+Global Instance duplicable_later P : Duplicable P → Duplicable (▷ P).
+Proof. rewrite /Duplicable => {1}->. by rewrite later_sep. Qed.
+Global Instance duplicable_laterN n P : Duplicable P → Duplicable (▷^n P).
+Proof. rewrite /Duplicable => {1}->. by rewrite laterN_sep. Qed.
+Global Instance duplicable_except_0 P : Duplicable P → Duplicable (◇ P).
+Proof. rewrite /Duplicable => {1}->. by rewrite except_0_sep. Qed.
+
 (** IntoAnd *)
 Global Instance into_and_later p P Q1 Q2 :
   IntoAnd p P Q1 Q2 → IntoAnd p (▷ P) (▷ Q1) (▷ Q2).
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index 84713ce14177f0dfec2039be135af958ef5a0cac..bb81d9826fc7d88d2d517ef17f6e898521a0122e 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -489,7 +489,7 @@ Proof.
     destruct rp.
     + rewrite (env_lookup_perm Γp) //= intuitionistically_and.
       by rewrite and_sep_intuitionistically -assoc.
-    + rewrite {1}intuitionistically_sep_dup {1}(env_lookup_perm Γp) //=.
+    + rewrite {1}(duplicable (□ _)) {1}(env_lookup_perm Γp) //=.
       by rewrite intuitionistically_and and_elim_l -assoc.
   - destruct (Γs !! i) eqn:?; simplify_eq/=.
     rewrite pure_True ?left_id; last (destruct Hwf; constructor;
diff --git a/theories/proofmode/frame_instances.v b/theories/proofmode/frame_instances.v
index 2dbbfd3a4e6f3918d04605262d8fd0ecd5ececa8..5000d20236f5c96cb1bea35ad8205b4ea87657da 100644
--- a/theories/proofmode/frame_instances.v
+++ b/theories/proofmode/frame_instances.v
@@ -87,7 +87,7 @@ Global Instance frame_sep_persistent_l progress R P1 P2 Q1 Q2 Q' :
   Frame true R (P1 ∗ P2) Q' | 9.
 Proof.
   rewrite /Frame /MaybeFrame /MakeSep /= => <- <- <-.
-  rewrite {1}(intuitionistically_sep_dup R). solve_sep_entails.
+  rewrite {1}(duplicable (â–¡ _)). solve_sep_entails.
 Qed.
 Global Instance frame_sep_l R P1 P2 Q Q' :
   Frame false R P1 Q → MakeSep Q P2 Q' → Frame false R (P1 ∗ P2) Q' | 9.