diff --git a/CHANGELOG.md b/CHANGELOG.md
index a7e0ac0c06018eb9e1c6ec17828b5c3cd310b85f..c3d325c75ad24146323128cde4f35b41a51cd1ae 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -110,15 +110,6 @@ 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`, `persistently_sep_dup`,
-  `plainly_sep_duplicable`, and `persistent_sep_dup` are now instances. This
-  means they are now uni-directional; use `duplicable_equiv` to obtain the
-  bidirectional version.
-  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`.
 * Remove the `gen_heap` notations `l ↦ -` and `l ↦{q} -`. They were barely used
   and looked very confusing in context: `l ↦ - ∗ P` looks like a magic wand.
 * Change `gen_inv_heap` notation `l ↦□ I` to `l ↦_I □`, so that `↦□` can be used
@@ -148,7 +139,6 @@ 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 0b728789cc87e1cce61bfd5851e570c653915767..b3f0cee87069a59a0f5b64e50a8e2832f1854a85 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -77,8 +77,6 @@ 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_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 d6f93ba166f4672a9e5f5f69945c3280eb2c24c0..d02ce530697f2199d52f6c924a832f6468d87a84 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -33,8 +33,6 @@ 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 76f570e234b2a430869bab2fee6d0e3da195abd1..adff4f6eb0a06733e346c854757bbc8bc6f9323a 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -97,9 +97,6 @@ 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).
@@ -148,12 +145,13 @@ Section inv.
     iMod "Hclose" as %_. iMod ("HcloseQ" with "HQ") as %_. by iApply "HcloseP".
   Qed.
 
-  Lemma inv_combine_dup_l P `{!Duplicable P} N Q :
+  Lemma inv_combine_dup_l N P Q :
+    □ (P -∗ P ∗ P) -∗
     inv N P -∗ inv N Q -∗ inv N (P ∗ Q).
   Proof.
-    rewrite inv_eq. iIntros "#HinvP #HinvQ !>" (E ?).
+    rewrite inv_eq. iIntros "#HPdup #HinvP #HinvQ !>" (E ?).
     iMod ("HinvP" with "[//]") as "[HP HcloseP]".
-    iDestruct (duplicable P with "HP") as "[$ HP]".
+    iDestruct ("HPdup" 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 f522aa8f132417fe11f71b75260cfa31ccc8a858..66684fb4d093b24c50a4faebf70fe4b73ce11001 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -193,8 +193,6 @@ 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 f40575296c48f42bb81ffa051e6e86ffca89f1e8..ea7b86b0d1b97add8dbf4e2e4327ffe3f72f51d1 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 (duplicable (□ _)) -assoc [(□ _ ∗ _)%I]comm -!assoc assoc.
+    rewrite intuitionistically_sep_dup -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,11 +210,13 @@ Section sep_list.
       apply forall_intro=> k. by rewrite (forall_elim (S k)).
   Qed.
 
-  Lemma big_sepL_dup P `{!Affine P, !Duplicable P} l :
-    P -∗ [∗ list] k↦x ∈ l, P.
+  Lemma big_sepL_dup P `{!Affine P} l :
+    □ (P -∗ P ∗ P) -∗ P -∗ [∗ list] k↦x ∈ l, P.
   Proof.
+    apply wand_intro_l.
     induction l as [|x l IH]=> /=; first by apply: affine.
-    rewrite {1}(duplicable P). apply sep_mono; done.
+    rewrite intuitionistically_sep_dup {1}intuitionistically_elim.
+    rewrite assoc wand_elim_r -assoc. apply sep_mono; done.
   Qed.
 
   Lemma big_sepL_delete Φ l i x :
@@ -267,16 +269,6 @@ 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.
@@ -565,7 +557,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 (duplicable (□ _)) -assoc [(□ _ ∗ _)%I]comm -!assoc assoc.
+    rewrite intuitionistically_sep_dup -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.
@@ -610,14 +602,6 @@ 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.
@@ -750,10 +734,6 @@ 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.
@@ -865,13 +845,6 @@ 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 *)
@@ -1055,7 +1028,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 // (duplicable (â–¡ _)).
+    rewrite !big_sepM_insert // intuitionistically_sep_dup.
     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.
@@ -1066,12 +1039,14 @@ Section map.
       by rewrite pure_True // True_impl.
   Qed.
 
-  Lemma big_sepM_dup P `{!Affine P, !Duplicable P} m :
-    P -∗ [∗ map] k↦x ∈ m, P.
+  Lemma big_sepM_dup P `{!Affine P} m :
+    □ (P -∗ P ∗ P) -∗ P -∗ [∗ map] k↦x ∈ m, P.
   Proof.
-    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.
+    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.
   Qed.
 
   Lemma big_sepM_later `{BiAffine PROP} Φ m :
@@ -1095,13 +1070,6 @@ 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.
@@ -1484,14 +1452,6 @@ 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.
@@ -1673,7 +1633,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 // (duplicable (â–¡ _)).
+    rewrite !big_sepS_insert // intuitionistically_sep_dup.
     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.
@@ -1682,11 +1642,14 @@ Section gset.
       by rewrite pure_True ?True_impl; last set_solver.
   Qed.
 
-  Lemma big_sepS_dup P `{!Affine P, !Duplicable P} X : P -∗ [∗ set] x ∈ X, P.
+  Lemma big_sepS_dup P `{!Affine P} X :
+    □ (P -∗ P ∗ P) -∗ P -∗ [∗ set] x ∈ X, P.
   Proof.
-    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.
+    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.
   Qed.
 
   Lemma big_sepS_later `{BiAffine PROP} Φ X :
@@ -1710,13 +1673,6 @@ 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 :
@@ -1829,13 +1785,6 @@ 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 40da60d3a1686cdcd7ddfb7bcfbd2c1eeeac155b..fdeb3a982771514003b786b90575c8b3ae70b39d 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -19,12 +19,6 @@ 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 17051f58886df272003dddb901ec1b99ae5f2452..5227d08edd7f4512516cd7f93c08a9eb82bd9c4b 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,10 +900,13 @@ Proof.
   rewrite persistently_forall_2. auto using persistently_mono, pure_intro.
 Qed.
 
-Global Instance persistently_sep_duplicable P : Duplicable (<pers> P).
+Lemma persistently_sep_dup P : <pers> P ⊣⊢ <pers> P ∗ <pers> P.
 Proof.
-  rewrite /Duplicable -{1}(idemp bi_and (<pers> _)%I).
-  by rewrite -{2}(emp_sep (<pers> _)%I) persistently_and_sep_assoc and_elim_l.
+  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.
 Qed.
 
 Lemma persistently_and_sep_l_1 P Q : <pers> P ∧ Q ⊢ <pers> P ∗ Q.
@@ -1100,10 +1103,9 @@ Proof.
   by rewrite -persistently_and_intuitionistically_sep_l -affinely_and affinely_and_r.
 Qed.
 
-Global Instance intuitionistically_sep_duplicable P : Duplicable (â–¡ P).
+Lemma intuitionistically_sep_dup P : □ P ⊣⊢ □ P ∗ □ P.
 Proof.
-  by rewrite /Duplicable -persistently_and_intuitionistically_sep_l
-    affinely_and_r idemp.
+  by rewrite -persistently_and_intuitionistically_sep_l affinely_and_r idemp.
 Qed.
 
 Lemma impl_wand_intuitionistically P Q : (<pers> P → Q) ⊣⊢ (□ P -∗ Q).
@@ -1113,11 +1115,12 @@ 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}(duplicable (â–¡ _)). apply sep_mono; last done.
+    rewrite {1}intuitionistically_sep_dup. 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.
@@ -1362,16 +1365,8 @@ Proof.
   - by rewrite persistent_and_affinely_sep_r_1 affinely_elim.
 Qed.
 
-(* Not an instance, see the bottom of this file *)
-Lemma persistent_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_sep_dup P `{!Persistent P, !Absorbing P} : P ⊣⊢ P ∗ P.
+Proof. by rewrite -(persistent_persistently P) -persistently_sep_dup. Qed.
 
 Lemma persistent_entails_l P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ Q ∗ P.
 Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
@@ -1538,58 +1533,6 @@ 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_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 |}.
@@ -1645,14 +1588,4 @@ Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A → PROP)
 Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
 End derived.
 
-(* When declared as an actual instance, [persistent_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_duplicable]. *)
-Hint Immediate persistent_duplicable : typeclass_instances.
-
 End bi.
diff --git a/theories/bi/derived_laws_later.v b/theories/bi/derived_laws_later.v
index 7c52a63516887cfbc485fe4f58fe6f5eb0a173db..a683467de724d154d0e9fc20e20c22eba4df1cec 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 -duplicable.
+    by rewrite -!or_intro_l -persistently_pure -later_sep -persistently_sep_dup.
   - 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 e3f358374b24f1057bb4549ba802e9b620cfa016..3ffb1d71f4332e5eba60fdfde98813cf1226f948 100644
--- a/theories/bi/internal_eq.v
+++ b/theories/bi/internal_eq.v
@@ -219,9 +219,6 @@ 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_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 c91b638922f6adc9308b27e49ca60487fcfdca41..04931d4c10fcea58363e1782fb7d97c4183939e4 100644
--- a/theories/bi/lib/fractional.v
+++ b/theories/bi/lib/fractional.v
@@ -63,24 +63,11 @@ 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.
-    (* FIXME: The hint for [persistent_duplicable] should apply here. *)
-    intros ? ? q q'. apply: bi.duplicable_equiv. apply: bi.persistent_duplicable.
-  Qed.
-  Global Instance duplicable_fractional P :
-    Duplicable P → Absorbing P → Fractional (λ _, P).
-  Proof. intros ? ? q q'. apply: bi.duplicable_equiv. Qed.
+  Proof. intros ?? q q'. by apply bi.persistent_sep_dup. 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 c977d532f3310d0ac29ae6584c80a6a2192dcea8..756dba593fd955d1b4067b4da66f758d15af765c 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -199,10 +199,12 @@ Qed.
 Lemma plainly_emp_2 : emp ⊢@{PROP} ■ emp.
 Proof. apply plainly_emp_intro. Qed.
 
-Global Instance plainly_sep_duplicable P : Duplicable (â–  P).
+Lemma plainly_sep_dup P : ■ P ⊣⊢ ■ P ∗ ■ P.
 Proof.
-  rewrite /Duplicable. rewrite -{1}(idemp bi_and (â–  _)%I).
-  by rewrite -{2}(emp_sep (â–  _)%I) plainly_and_sep_assoc and_elim_l.
+  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.
 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 ea989e6fa92446009267f6d7b1a05036246e68cb..2bef8b0e78e131b20140a3b57642ac86d031419f 100644
--- a/theories/bi/telescopes.v
+++ b/theories/bi/telescopes.v
@@ -84,9 +84,6 @@ 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 77baee77f0a21d23ec77a299a75d586be2896908..ffab7068c7775a9012011705441a422f8b652f5c 100644
--- a/theories/proofmode/class_instances_later.v
+++ b/theories/proofmode/class_instances_later.v
@@ -77,14 +77,6 @@ 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 bb81d9826fc7d88d2d517ef17f6e898521a0122e..84713ce14177f0dfec2039be135af958ef5a0cac 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}(duplicable (□ _)) {1}(env_lookup_perm Γp) //=.
+    + rewrite {1}intuitionistically_sep_dup {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 5000d20236f5c96cb1bea35ad8205b4ea87657da..2dbbfd3a4e6f3918d04605262d8fd0ecd5ececa8 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}(duplicable (â–¡ _)). solve_sep_entails.
+  rewrite {1}(intuitionistically_sep_dup R). 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.