diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5023d88ee9089cc03ff07746c59d3a82a5c14f42..8df954bc5712d8e07e707d645e553faedd6958c5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -74,34 +74,6 @@ Coq 8.13 is no longer supported.
     particular, replace `apply` by `iApply`).
   - Add some `apply bi.entails_wand`/`apply bi.wand_entails` to 'convert'
     between the old and new way of interpreting `P -∗ Q`.
-* Add the class of `Separable` propositions, which generalizes `Persistent`
-  propositions. The class will be useful when we introduce BIs with a
-  degenerative persistence modality, i.e., BIs without the proof rule
-  `True ⊢ <pers> True`/BIs with `<pers> P := False`.
-* Generalize lemmas about `persistently`/`plainly`/`Plain` to `Separable`:
-  + `persistently_and_sep_assoc`, `persistent_and_sep_assoc`,
-    `plainly_and_sep_assoc` → `and_sep_assoc`
-  + `persistently_sep_dup`, `persistent_sep_dup`, `plainly_sep_dup` → `sep_dup`
-  + `persistently_and_sep_l_1`, `plainly_and_sep_l_1` → `and_sep_l_1`
-  + `persistently_and_sep_r_1`, `plainly_and_sep_r_1` → `and_sep_l_1`
-  + `persistently_and_sep_l`, `plainly_and_sep_l` → `and_sep_l`
-  + `persistently_and_sep_r`, `plainly_and_sep_r` → `and_sep_r`
-  + `persistent_and_sep_1` → `and_sep_1`
-  + `persistent_and_sep`, `and_sep_persistently`, `and_sep_plainly` → `and_sep`
-  + `persistently_entails_l`, `persistent_entails_l`, `plainly_entails_l` →
-    `entails_l`
-  + `persistently_entails_r`, `persistent_entails_r`, `plainly_entails_r` →
-    `entails_r`
-  + `impl_wand_persistently_2`, `impl_wand_plainly_2` → `impl_wand_2`
-  + `impl_wand_persistently`, `impl_wand_plainly` → `impl_wand`
-  + `persistent_and_affinely_sep_l_1` → `and_affinely_sep_l_1`
-  + `persistent_and_affinely_sep_r_1` → `and_affinely_sep_r_1`
-  + `persistent_and_affinely_sep_l` → `and_affinely_sep_l`
-  + `persistent_and_affinely_sep_r` → `and_affinely_sep_r`
-  + `persistent_absorbingly_affinely_2` → `absorbingly_affinely_2`
-  + `persistent_absorbingly_affinely` → `absorbingly_affinely`
-  + `persistent_impl_wand_affinely`, `impl_wand_affinely_plainly` →
-    `impl_affinely_wand`
 
 **Changes in `proofmode`:**
 
@@ -173,17 +145,6 @@ s/\bloc_add(_assoc|_0|_inj|)\b/Loc.add\1/g
 s/\bfresh_locs(_fresh|)\b/Loc.fresh\1/g
 # unseal
 s/\bMonPred\.unseal\b/monPred\.unseal/g
-# separable
-s/\b(persistently|persistent|plainly)_and_sep_assoc\b/and_sep_assoc/g
-s/\b(persistently|persistent|plainly)_sep_dup\b/sep_dup/g
-s/\b(persistently|plainly)_and_sep_(l_1|r_1|l|r)\b/and_sep_\2/g
-s/\bpersistent_and_sep_1\b/and_sep_1/g
-s/\b(persistent_and_sep|and_sep_persistently|and_sep_plainly)\b/and_sep/g
-s/\b(persistently|persistent|plainly)_entails_(l|r)\b/entails_\2/g
-s/\bimpl_wand_(persistently|plainly)(|_2)\b/impl_wand\2/g
-s/\bpersistent_and_affinely_sep_(l_1|r_1|l|r)\b/and_affinely_sep_\1/g
-s/\bpersistent_absorbingly_affinely(|_2)\b/absorbingly_affinely\1/g
-s/\b(persistent_impl_wand_affinely|impl_wand_affinely_plainly)\b/impl_affinely_wand/g
 EOF
 ```
 
diff --git a/docs/classes.md b/docs/classes.md
deleted file mode 100644
index d37d1cbbf3a0a15a1701c157f30b3220eccb5e7f..0000000000000000000000000000000000000000
--- a/docs/classes.md
+++ /dev/null
@@ -1,99 +0,0 @@
-# Type classes
-
-This file collects conventions about the use of type classes in Iris.
-The file is work in progress, so many conventions are missing and remain to be
-documented.
-
-## Order of `TCOr` arguments
-
-We often use the `TCOr` combinator (from std++) to describe disjunctive type
-class premises. For example:
-
-```coq
-Lemma sep_elim_l P Q `{!TCOr (Affine Q) (Absorbing P)} : P ∗ Q ⊢ P.
-```
-
-Type class search will only introduce `TCOr`, but never eliminate `TCOr`.
-As such, to make it easy to derive other lemmas that use `TCOr`, it is important
-that the arguments of `TCOr` are in a consistent order. For example:
-
-```coq
-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 `{!TCOr (Affine P) (Absorbing Q), !TCOr (Affine Q) (Absorbing P)} : P ∗ Q ⊢ P ∧ Q.
-Proof. apply and_intro; [apply: sep_elim_l|apply: sep_elim_r]. Qed.
-```
-
-As shown here, it is not needed to eliminate (i.e., `destruct`) the `TCOr`
-because the order matches up.
-
-**Conventions:**
-
-- Affine before absorbing, i.e., `TCOr (Affine P) (Absorbing Q)`
-
-## Use of `Hint Cut` to prune the search space
-
-We often use type classes to describe classes of objects that satisfy some
-property. For example, `Persistent` and `Separable` describe the BI propositions
-that are persistent and separable. There is an inheritance between the two
-classes, and both are closed under the usual logical connectives, resulting in
-the instances:
-
-```coq
-Instance persistent_separable P : Persistent P → Separable P.
-Instance and_persistent P Q : Persistent P → Persistent Q → Persistent (P ∧ Q).
-Instance and_separable P1 P2 : Separable P1 → Separable P2 → Separable (P1 ∧ P2).
-```
-
-Having these instances at the same time is problematic since there might be
-multiple derivations for the same goal. For example:
-
-```
-Persistent P        Persistent Q              Persistent P         Persistent Q
-------------        ------------              ---------------------------------
-Separable P         Separable Q                    Persistent (P ∧ Q)
-        -----------------                          ------------------
-        Separable (P ∧ Q)                           Separable (P ∧ Q)
-```
-
-When considering `P1 ∧ ... ∧ Pn`, the number of derivations is `O(n^2)`.
-When adding an additional class, e.g., `Plain` for which we have
-`Plain P → Persistent P`, the number of derivation becomes `O(n^3)`. This makes
-failing searches very inefficient because the whole search needs to be explored
-to conclude that the goal cannot be derived.
-
-In the above, we see that the second derivation is redundant, so we should thus
-exclude it. We do this using the following `Hint Cut` declaration:
-
-```coq
-Global Hint Cut [_* persistent_separable and_persistent] : typeclass_instances.
-```
-
-This hint says that at any point during the instance search (`_*`), if
-`persistent_separable` has been applied, the next instance to be applied should
-**not** be `and_persistent`. This rules out the derivation on the right
-in the example above.
-
-**Warning from the Coq reference manual:** The regexp matches the entire path.
-Most hints will start with a leading `_*` to match the tail of the path.
-
-The order matters. Having a cut for `[_* and_persistent persistent_separable]`
-(i.e., excluding the first derivation) would result in incompleteness. It
-becomes impossible to derive `Separable (P ∧ Q)` from `Persistent P` and
-`Separable Q`.
-
-Note that `Separable` is not closed under `∀`, but `Persistent` is. Hence we
-should **not** have a cut `[_* persistent_separable forall_persistent]`. This
-cut would make it impossible to derive `Separable (∀ x, Φ x)` from
-`∀ x, Persistent (Φ x)`.
-
-**General principle:** For any "class inheritance" instance `C1_C2` from `C1` to
-`C2` and "class closed under connective" instance `op_C1` for `C1` such that
-`C2` also has a closedness instance `op_C2` for the same connective, we cut
-`[_* C1_C2 op_C1]`.
-
-The principle also works when having chains of inheritance instances, e.g., `C1`
-to `C2` to `C3`. It is important to not add instances for the transitive
-inheritances, i.e., from `C1` to `C3`.
-
diff --git a/iris/base_logic/lib/own.v b/iris/base_logic/lib/own.v
index 520afde7883f11d2beb2b0826eea2b8efa3c8332..2be0458d2b628c0a3d47e2d5523c6099eec15e98 100644
--- a/iris/base_logic/lib/own.v
+++ b/iris/base_logic/lib/own.v
@@ -185,7 +185,7 @@ Proof. apply entails_wand, wand_intro_r. by rewrite -own_op own_valid. Qed.
 Lemma own_valid_3 γ a1 a2 a3 : own γ a1 -∗ own γ a2 -∗ own γ a3 -∗ ✓ (a1 ⋅ a2 ⋅ a3).
 Proof. apply entails_wand. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed.
 Lemma own_valid_r γ a : own γ a ⊢ own γ a ∗ ✓ a.
-Proof. apply: bi.entails_r. apply own_valid. Qed.
+Proof. apply: bi.persistent_entails_r. apply own_valid. Qed.
 Lemma own_valid_l γ a : own γ a ⊢ ✓ a ∗ own γ a.
 Proof. by rewrite comm -own_valid_r. Qed.
 
@@ -271,7 +271,7 @@ Proof.
     { apply inG_unfold_validN. }
     by apply cmra_transport_updateP'.
   - apply exist_elim=> m; apply pure_elim_l=> -[a' [-> HP]].
-    rewrite -(exist_intro a'). rewrite -and_sep.
+    rewrite -(exist_intro a'). rewrite -persistent_and_sep.
     by apply and_intro; [apply pure_intro|].
 Qed.
 
@@ -392,6 +392,6 @@ Section proofmode_instances.
     FromAnd (own γ a) (own γ b1) (own γ b2).
   Proof.
     intros ? Hb. rewrite /FromAnd (is_op a) own_op.
-    destruct Hb; by rewrite and_sep.
+    destruct Hb; by rewrite persistent_and_sep.
   Qed.
 End proofmode_instances.
diff --git a/iris/base_logic/proofmode.v b/iris/base_logic/proofmode.v
index 30f3dd3e57333e225cf7baf2daf97866d0df1164..01cfda35479376f2726f5df5b16b351fb188c53a 100644
--- a/iris/base_logic/proofmode.v
+++ b/iris/base_logic/proofmode.v
@@ -43,7 +43,7 @@ Section class_instances.
     FromAnd (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
   Proof.
     intros ? H. rewrite /FromAnd (is_op a) ownM_op.
-    destruct H; by rewrite bi.and_sep.
+    destruct H; by rewrite bi.persistent_and_sep.
   Qed.
 
   Global Instance into_and_ownM p (a b1 b2 : M) :
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 3725368d8641dc386c102f38e6462ed9c0c45200..ad7d004d3ec9cf1b55615172ecd891f790128724 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -250,7 +250,7 @@ Section sep_list.
     induction l as [|x l IH] using rev_ind.
     { rewrite big_sepL_nil. apply affinely_elim_emp. }
     rewrite big_sepL_snoc // -IH.
-    rewrite -and_sep_1 -affinely_and -pure_and.
+    rewrite -persistent_and_sep_1 -affinely_and -pure_and.
     f_equiv. f_equiv=>- Hlx. split.
     - intros k y Hy. apply Hlx. rewrite lookup_app Hy //.
     - apply Hlx. rewrite lookup_app lookup_ge_None_2 //.
@@ -289,7 +289,7 @@ Section sep_list.
       apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepL_lookup. }
     revert Φ HΦ. induction l as [|x l IH]=> Φ HΦ /=.
     { apply: affine. }
-    rewrite -and_sep_1. apply and_intro.
+    rewrite -persistent_and_sep_1. apply and_intro.
     - rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl. done.
     - rewrite -IH. apply forall_intro => k. by rewrite (forall_elim (S k)).
   Qed.
@@ -698,10 +698,10 @@ Section sep_list2.
     ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2 ∗ Ψ k y1 y2)
     ⊣⊢ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ∗ ([∗ list] k↦y1;y2 ∈ l1;l2, Ψ k y1 y2).
   Proof.
-    rewrite !big_sepL2_alt big_sepL_sep !and_affinely_sep_l.
+    rewrite !big_sepL2_alt big_sepL_sep !persistent_and_affinely_sep_l.
     rewrite -assoc (assoc _ _ (<affine> _)%I). rewrite -(comm bi_sep (<affine> _)%I).
-    rewrite -assoc (assoc _ _ (<affine> _)%I) -!and_affinely_sep_l.
-    by rewrite affinely_and_r and_affinely_sep_l idemp.
+    rewrite -assoc (assoc _ _ (<affine> _)%I) -!persistent_and_affinely_sep_l.
+    by rewrite affinely_and_r persistent_and_affinely_sep_l idemp.
   Qed.
 
   Lemma big_sepL2_sep_2 Φ Ψ l1 l2 :
@@ -786,7 +786,7 @@ Section sep_list2.
     apply pure_elim_l=> Hlen.
     revert l2 Φ HΦ Hlen. induction l1 as [|x1 l1 IH]=> -[|x2 l2] Φ HΦ Hlen; simplify_eq/=.
     { by apply (affine _). }
-    rewrite -and_sep_1. apply and_intro.
+    rewrite -persistent_and_sep_1. apply and_intro.
     - rewrite (forall_elim 0) (forall_elim x1) (forall_elim x2).
       by rewrite !pure_True // !True_impl.
     - rewrite -IH //.
@@ -930,7 +930,7 @@ Lemma big_sepL2_sep_sepL_l {A B} (Φ : nat → A → PROP)
 Proof.
   rewrite big_sepL2_sep big_sepL2_const_sepL_l. apply (anti_symm _).
   { rewrite and_elim_r. done. }
-  rewrite !big_sepL2_alt [(_ ∗ _)%I]comm -!and_sep_assoc.
+  rewrite !big_sepL2_alt [(_ ∗ _)%I]comm -!persistent_and_sep_assoc.
   apply pure_elim_l=>Hl. apply and_intro.
   { apply pure_intro. done. }
   rewrite [(_ ∗ _)%I]comm. apply sep_mono; first done.
@@ -1254,7 +1254,7 @@ Section or_list.
   Proof.
     rewrite !big_orL_exist sep_exist_l.
     f_equiv=> k. rewrite sep_exist_l. f_equiv=> x.
-    by rewrite !and_affinely_sep_l !assoc (comm _ P).
+    by rewrite !persistent_and_affinely_sep_l !assoc (comm _ P).
  Qed.
   Lemma big_orL_sep_r Q Φ l :
     ([∨ list] k↦x ∈ l, Φ k x) ∗ Q ⊣⊢ ([∨ list] k↦x ∈ l, Φ k x ∗ Q).
@@ -1499,7 +1499,7 @@ Section sep_map.
     induction m as [|k x m ? IH] using map_ind.
     { rewrite big_sepM_empty. apply affinely_elim_emp. }
     rewrite big_sepM_insert // -IH.
-    by rewrite -and_sep_1 -affinely_and -pure_and map_Forall_insert.
+    by rewrite -persistent_and_sep_1 -affinely_and -pure_and map_Forall_insert.
   Qed.
   (** The general backwards direction requires [BiAffine] to cover the empty case. *)
   Lemma big_sepM_pure `{!BiAffine PROP} (φ : K → A → Prop) m :
@@ -1537,7 +1537,7 @@ Section sep_map.
       apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepM_lookup. }
     revert Φ HΦ. induction m as [|i x m ? IH] using map_ind=> Φ HΦ.
     { rewrite big_sepM_empty. apply: affine. }
-    rewrite big_sepM_insert // -and_sep_1. apply and_intro.
+    rewrite big_sepM_insert // -persistent_and_sep_1. apply and_intro.
     - rewrite (forall_elim i) (forall_elim x) lookup_insert.
       by rewrite pure_True // True_impl.
     - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
@@ -2048,7 +2048,7 @@ Section map2.
     intros Hm1 Hm2. rewrite !big_sepM2_alt -map_insert_zip_with.
     rewrite big_sepM_insert;
       last by rewrite map_lookup_zip_with Hm1.
-    rewrite !and_affinely_sep_l /=.
+    rewrite !persistent_and_affinely_sep_l /=.
     rewrite sep_assoc (sep_comm _ (Φ _ _ _)) -sep_assoc.
     repeat apply sep_proper=>//.
     apply affinely_proper, pure_proper.
@@ -2067,7 +2067,7 @@ Section map2.
       Φ i x1 x2 ∗ [∗ map] k↦x;y ∈ delete i m1;delete i m2, Φ k x y.
   Proof.
     rewrite !big_sepM2_alt=> Hx1 Hx2.
-    rewrite !and_affinely_sep_l /=.
+    rewrite !persistent_and_affinely_sep_l /=.
     rewrite sep_assoc (sep_comm  (Φ _ _ _)) -sep_assoc.
     apply sep_proper.
     - apply affinely_proper, pure_proper. split.
@@ -2154,7 +2154,7 @@ Section map2.
     assert (TCOr (∀ x, Affine (Φ i x.1 x.2)) (Absorbing (Φ i x1 x2))).
     { destruct select (TCOr _ _); apply _. }
     apply entails_wand, wand_intro_r.
-    rewrite !and_affinely_sep_l /=.
+    rewrite !persistent_and_affinely_sep_l /=.
     rewrite (sep_comm  (Φ _ _ _)) -sep_assoc. apply sep_mono.
     { apply affinely_mono, pure_mono. intros Hm k.
       rewrite !lookup_insert_is_Some. naive_solver. }
@@ -2249,7 +2249,7 @@ Section map2.
     rewrite !big_sepM2_alt.
     rewrite -{1}(idemp bi_and ⌜∀ k : K, is_Some (m1 !! k) ↔ is_Some (m2 !! k)⌝%I).
     rewrite -assoc.
-    rewrite !and_affinely_sep_l /=.
+    rewrite !persistent_and_affinely_sep_l /=.
     rewrite -assoc. apply sep_proper=>//.
     rewrite assoc (comm _ _ (<affine> _)%I) -assoc.
     apply sep_proper=>//. apply big_sepM_sep.
@@ -2724,7 +2724,7 @@ Section gset.
     induction X as [|x X ? IH] using set_ind_L.
     { rewrite big_sepS_empty. apply affinely_elim_emp. }
     rewrite big_sepS_insert // -IH.
-    rewrite -and_sep_1 -affinely_and -pure_and.
+    rewrite -persistent_and_sep_1 -affinely_and -pure_and.
     f_equiv. f_equiv=>HX. split.
     - apply HX. set_solver+.
     - apply set_Forall_union_inv_2 in HX. done.
@@ -2764,7 +2764,7 @@ Section gset.
       apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepS_elem_of. }
     revert Φ HΦ. induction X as [|x X ? IH] using set_ind_L=> Φ HΦ.
     { rewrite big_sepS_empty. apply: affine. }
-    rewrite big_sepS_insert // -and_sep_1. apply and_intro.
+    rewrite big_sepS_insert // -persistent_and_sep_1. apply and_intro.
     - rewrite (forall_elim x) pure_True ?True_impl; last set_solver. done.
     - rewrite -IH. apply forall_mono=> y.
       apply impl_intro_l, pure_elim_l=> ?.
@@ -2984,7 +2984,7 @@ Section gmultiset.
     induction X as [|x X IH] using gmultiset_ind.
     { rewrite big_sepMS_empty. apply affinely_elim_emp. }
     rewrite big_sepMS_insert // -IH.
-    rewrite -and_sep_1 -affinely_and -pure_and.
+    rewrite -persistent_and_sep_1 -affinely_and -pure_and.
     f_equiv. f_equiv=>HX. split.
     - apply HX. set_solver+.
     - intros y Hy. apply HX. multiset_solver.
@@ -3026,7 +3026,7 @@ Section gmultiset.
     revert Φ HΦ. induction X as [|x X IH] using gmultiset_ind=> Φ HΦ.
     { rewrite big_sepMS_empty. apply: affine. }
     rewrite big_sepMS_disj_union.
-    rewrite big_sepMS_singleton -and_sep_1. apply and_intro.
+    rewrite big_sepMS_singleton -persistent_and_sep_1. apply and_intro.
     - rewrite (forall_elim x) pure_True ?True_impl; last multiset_solver. done.
     - rewrite -IH. apply forall_mono=> y.
       apply impl_intro_l, pure_elim_l=> ?.
diff --git a/iris/bi/derived_connectives.v b/iris/bi/derived_connectives.v
index bbf1d1029933ace927d854275ed5a70e82dc5afd..a5f5d62b307d37a701303d1f47e8b93bf65c7a0b 100644
--- a/iris/bi/derived_connectives.v
+++ b/iris/bi/derived_connectives.v
@@ -76,26 +76,6 @@ Global Instance: Params (@bi_intuitionistically_if) 2 := {}.
 Global Typeclasses Opaque bi_intuitionistically_if.
 Notation "'â–¡?' p P" := (bi_intuitionistically_if p P) : bi_scope.
 
-(* The class of [Separable] propositions generalizes [bi_pure] and [Persistent]
-propositions. Being separable implies being duplicable, but it is strictly
-stronger than that: [P := ∃ q, l ↦{q} v] is duplicable but not separable.
-Counterexample: [P ∧ l ↦ v] does not entail [P ∗ l ↦ v]. Therefore, the
-hierarchy is: Plain → Persistent → Separable → Duplicable.
-
-The class of [Separable] propositions is useful for BIs with a degenerative
-persistence modality, i.e., without [BiPersistentlyTrue : True ⊢ <pers> True],
-see https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/843. For those BIs,
-the only persistent proposition is [False], but emp/plain and friends are still
-[Separable].
-
-Note that the reverse direction [<affine> P ∗ Q ⊢ <absorb> P ∧ Q] is a
-tautology, see [affinely_sep_absorbingly_and] in [derived_laws]. *)
-Class Separable {PROP : bi} (P : PROP) :=
-  separable Q : <absorb> P ∧ Q ⊢ <affine> P ∗ Q.
-Global Arguments Separable {_} _%I : simpl never.
-Global Arguments separable {_} _%I.
-Global Hint Mode Separable + ! : typeclass_instances.
-
 Fixpoint bi_laterN {PROP : bi} (n : nat) (P : PROP) : PROP :=
   match n with
   | O => P
diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index ad3c29306a9f33472625158567cb6a9bee8dbe12..4774449d809211a1b4f118753103ad15e0551c0f 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -733,19 +733,22 @@ Proof.
   rewrite -(absorbing emp) absorbingly_sep_l left_id //.
 Qed.
 
-Lemma sep_elim_l P Q `{!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 select (TCOr _ _).
+  destruct HQP.
   - by rewrite (affine Q) right_id.
   - by rewrite (True_intro Q) comm.
 Qed.
-Lemma sep_elim_r P Q `{!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
-    `{!TCOr (Affine P) (Absorbing Q), !TCOr (Affine Q) (Absorbing P)} :
+Lemma sep_and P Q :
+  TCOr (Affine P) (Absorbing Q) → TCOr (Affine Q) (Absorbing P) →
   P ∗ Q ⊢ P ∧ Q.
-Proof. apply and_intro; [apply: sep_elim_l|apply: sep_elim_r]. Qed.
+Proof.
+  intros [?|?] [?|?];
+    apply and_intro; apply: sep_elim_l || apply: sep_elim_r.
+Qed.
 
 Lemma affinely_intro P Q `{!Affine P} : (P ⊢ Q) → P ⊢ <affine> Q.
 Proof. intros <-. by rewrite affine_affinely. Qed.
@@ -798,185 +801,6 @@ Section bi_affine.
   Proof. apply wand_intro_l. by rewrite sep_and impl_elim_r. Qed.
 End bi_affine.
 
-(* Separable propositions *)
-(** This lemma shows that the reverse direction of [Separable] is a tautology. *)
-Lemma affinely_sep_absorbingly_and P Q : <affine> P ∗ Q ⊢ <absorb> P ∧ Q.
-Proof.
-  apply and_intro.
-  - rewrite affinely_elim (comm _ P). apply sep_mono; auto.
-  - by rewrite sep_elim_r.
-Qed.
-
-Lemma and_affinely_sep_l_1 P Q `{!Separable P} :
-  P ∧ Q ⊢ <affine> P ∗ Q.
-Proof. by rewrite -separable -absorbingly_intro. Qed.
-Lemma and_affinely_sep_r_1 P Q `{!Separable P} :
-  Q ∧ P ⊢ Q ∗ <affine> P.
-Proof. by rewrite !(comm _ Q) and_affinely_sep_l_1. Qed.
-
-Lemma absorbingly_and_sep_l_1 P Q `{!Separable P} :
-  <absorb> P ∧ Q ⊢ P ∗ Q.
-Proof. by rewrite separable affinely_elim. Qed.
-Lemma absorbingly_and_sep_r_1 P Q `{!Separable P} :
-  Q ∧ <absorb> P ⊢ Q ∗ P.
-Proof. by rewrite !(comm _ Q) absorbingly_and_sep_l_1. Qed.
-
-Lemma and_affinely_sep_l P Q `{!Separable P, !TCOr (Affine Q) (Absorbing P)} :
-  P ∧ Q ⊣⊢ <affine> P ∗ Q.
-Proof.
-  apply (anti_symm (⊢)); first by apply and_affinely_sep_l_1. apply and_intro.
-  - by rewrite affinely_elim sep_elim_l.
-  - rewrite affinely_elim_emp left_id. done.
-Qed.
-Lemma and_affinely_sep_r P Q `{!Separable P, !TCOr (Affine Q) (Absorbing P)} :
-  Q ∧ P ⊣⊢ Q ∗ <affine> P.
-Proof. by rewrite !(comm _ Q) and_affinely_sep_l. Qed.
-
-Lemma absorbingly_and_sep_l P Q `{!Separable P, !TCOr (Affine P) (Absorbing Q)} :
-  <absorb> P ∧ Q ⊣⊢ P ∗ Q.
-Proof.
-  apply (anti_symm (⊢)); first by apply absorbingly_and_sep_l_1. apply and_intro.
-  - rewrite (comm _ P). rewrite /bi_absorbingly. auto.
-  - by rewrite sep_elim_r.
-Qed.
-Lemma absorbingly_and_sep_r P Q `{!Separable P, !TCOr (Affine P) (Absorbing Q)} :
-  Q ∧ <absorb> P ⊣⊢ Q ∗ P.
-Proof. by rewrite !(comm _ Q) absorbingly_and_sep_l. Qed.
-
-Lemma and_sep_assoc P Q R `{!Separable P, !Absorbing P} :
-  P ∧ (Q ∗ R) ⊣⊢ (P ∧ Q) ∗ R.
-Proof. rewrite and_affinely_sep_l // assoc. rewrite -and_affinely_sep_l //. Qed.
-Lemma sep_and_assoc P Q R `{!Separable P, !Affine P} :
-  P ∗ (Q ∧ R) ⊣⊢ (P ∗ Q) ∧ R.
-Proof. by rewrite -absorbingly_and_sep_l assoc absorbingly_and_sep_l. Qed.
-
-Lemma absorbingly_affinely_2 P `{!Separable P} :
-  P ⊢ <absorb> <affine> P.
-Proof. by rewrite -{1}(left_id True%I bi_and P) and_affinely_sep_r_1. Qed.
-Lemma absorbingly_affinely P `{!Separable P, !Absorbing P} :
-  <absorb> <affine> P ⊣⊢ P.
-Proof.
-  rewrite /bi_absorbingly /bi_affinely.
-  rewrite [(_ ∧ _)%I]comm [(_ ∗ _)%I]comm -and_sep_assoc //.
-  rewrite left_id right_id //.
-Qed.
-
-Lemma affinely_absorbingly_1 P `{!Separable P} :
-  <affine> <absorb> P ⊢ P.
-Proof. by rewrite /bi_affinely absorbingly_and_sep_r_1 left_id. Qed.
-Lemma affinely_absorbing P `{!Separable P, !Affine P} :
-  <affine> <absorb> P ⊣⊢ P.
-Proof.
-  rewrite /bi_absorbingly /bi_affinely.
-  rewrite [(_ ∧ _)%I]comm [(_ ∗ _)%I]comm -sep_and_assoc //.
-  rewrite left_id right_id //.
-Qed.
-
-Lemma impl_affinely_wand P Q `{!Separable P, !Absorbing P} :
-  (P → Q) ⊣⊢ (<affine> P -∗ Q).
-Proof.
-  apply (anti_symm _).
-  - apply wand_intro_l. rewrite -and_affinely_sep_l // impl_elim_r //.
-  - apply impl_intro_l. rewrite and_affinely_sep_l // wand_elim_r //.
-Qed.
-Lemma absorbingly_impl_wand P Q `{!Separable P, !Affine P} :
-  (<absorb> P → Q) ⊣⊢ (P -∗ Q).
-Proof.
-  apply (anti_symm _).
-  - apply wand_intro_l. rewrite -absorbingly_and_sep_l // impl_elim_r //.
-  - apply impl_intro_l. rewrite absorbingly_and_sep_l // wand_elim_r //.
-Qed.
-
-Lemma and_sep_l_1 P Q `{!Separable P} : P ∧ Q ⊢ P ∗ Q.
-Proof. by rewrite and_affinely_sep_l_1 affinely_elim. Qed.
-Lemma and_sep_r_1 P Q `{!Separable Q} : P ∧ Q ⊢ P ∗ Q.
-Proof. by rewrite and_affinely_sep_r_1 affinely_elim. Qed.
-Lemma and_sep_1 P Q `{HPQ : !TCOr (Separable P) (Separable Q)} :
-  P ∧ Q ⊢ P ∗ Q.
-Proof. destruct HPQ; [apply: and_sep_l_1|apply: and_sep_r_1]. Qed.
-
-Lemma and_sep_l P Q `{!Separable P}
-    `{!TCOr (Affine P) (Absorbing Q), !TCOr (Affine Q) (Absorbing P)} :
-  P ∧ Q ⊣⊢ P ∗ Q.
-Proof. apply (anti_symm (⊢)); [apply: and_sep_l_1|apply: sep_and]. Qed.
-Lemma and_sep_r P Q `{!Separable Q}
-    `{!TCOr (Affine P) (Absorbing Q), !TCOr (Affine Q) (Absorbing P)} :
-  P ∧ Q ⊣⊢ P ∗ Q.
-Proof. by rewrite !(comm _ P) and_sep_l. Qed.
-Lemma and_sep P Q `{!TCOr (Separable P) (Separable Q)}
-    `{!TCOr (Affine P) (Absorbing Q), !TCOr (Affine Q) (Absorbing P)} :
-  P ∧ Q ⊣⊢ P ∗ Q.
-Proof.
-  destruct select (TCOr (Separable _) _); [apply: and_sep_l|apply: and_sep_r].
-Qed.
-
-Lemma sep_dup P `{!Separable P, !TCOr (Affine P) (Absorbing P)} :
-  P ⊣⊢ P ∗ P.
-Proof. by rewrite -{1}(idemp bi_and P) and_sep. Qed.
-
-Lemma impl_wand_2 P Q `{!Separable P} : (P -∗ Q) ⊢ (P → Q).
-Proof.
-  apply impl_intro_l. rewrite and_affinely_sep_l_1.
-  by rewrite affinely_elim wand_elim_r.
-Qed.
-
-Lemma entails_l P Q `{!Separable Q} : (P ⊢ Q) → P ⊢ Q ∗ P.
-Proof. intros. rewrite -and_sep_1; auto. Qed.
-Lemma entails_r P Q `{!Separable Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
-Proof. intros. rewrite -and_sep_1; auto. Qed.
-
-Section separable_affine_bi.
-  Context `{!BiAffine PROP}.
-
-  Lemma impl_wand P Q `{!Separable P} : (P → Q) ⊣⊢ (P -∗ Q).
-  Proof. apply (anti_symm (⊢)); [apply impl_wand_1|apply: impl_wand_2]. Qed.
-End separable_affine_bi.
-
-Global Instance impl_absorbing P Q :
-  Separable P → Absorbing P → Absorbing Q → Absorbing (P → Q).
-Proof.
-  intros. rewrite /Absorbing. apply impl_intro_l.
-  rewrite and_affinely_sep_l_1 absorbingly_sep_r.
-  by rewrite -and_affinely_sep_l impl_elim_r.
-Qed.
-
-(* Separable instances *)
-Global Instance emp_separable : Separable (PROP:=PROP) emp.
-Proof. intros Q. by rewrite affinely_emp left_id and_elim_r. Qed.
-Global Instance and_separable P1 P2 :
-  Separable P1 → Separable P2 → Separable (P1 ∧ P2).
-Proof.
-  intros ?? Q. rewrite absorbingly_and_1 -assoc 2!separable assoc.
-  by rewrite sep_and affinely_and.
-Qed.
-Global Instance exist_separable {A} (Φ : A → PROP) :
-  (∀ x, Separable (Φ x)) → Separable (∃ x, Φ x).
-Proof.
-  intros ? Q. rewrite absorbingly_exist and_exist_r. apply exist_elim=> x.
-  by rewrite -(exist_intro x) separable.
-Qed.
-Global Instance or_separable P1 P2 :
-  Separable P1 → Separable P2 → Separable (P1 ∨ P2).
-Proof.
-  intros ?? Q. rewrite absorbingly_or affinely_or.
-  by rewrite and_or_r sep_or_r 2!separable.
-Qed.
-Global Instance sep_separable P1 P2 :
-  Separable P1 → Separable P2 → Separable (P1 ∗ P2).
-Proof.
-  intros ?? Q. rewrite absorbingly_sep sep_and -assoc 2!separable assoc.
-  by rewrite affinely_sep_2.
-Qed.
-Global Instance affinely_separable P : Separable P → Separable (<affine> P).
-Proof. rewrite /bi_affinely. apply _. Qed.
-Global Instance absorbingly_separable P : Separable P → Separable (<absorb> P).
-Proof.
-  intros ? Q. by rewrite absorbingly_idemp separable -absorbingly_intro.
-Qed.
-Global Instance from_option_separable {A} P (Ψ : A → PROP) (mx : option A) :
-  (∀ x, Separable (Ψ x)) → Separable P → Separable (from_option Ψ P mx).
-Proof. destruct mx; apply _. Qed.
-
 (* Pure stuff *)
 Lemma pure_elim φ Q R : (Q ⊢ ⌜φ⌝) → (φ → Q ⊢ R) → Q ⊢ R.
 Proof.
@@ -1076,12 +900,6 @@ Proof.
   rewrite -decide_bi_True. destruct (decide _); [done|]. by rewrite True_emp.
 Qed.
 
-Global Instance pure_separable {φ} : Separable (PROP:=PROP) ⌜φ⌝.
-Proof.
-  intros Q. rewrite absorbingly_pure. apply pure_elim_l=> ?.
-  rewrite pure_True // affinely_True_emp left_id. done.
-Qed.
-
 (* Properties of the persistence modality *)
 Local Hint Resolve persistently_mono : core.
 Global Instance persistently_mono' : Proper ((⊢) ==> (⊢)) (@bi_persistently PROP).
@@ -1152,20 +970,23 @@ Proof.
   apply persistently_and_sep_elim.
 Qed.
 
-(** High cost, should only be used if no other [Separable] instances can be
-applied *)
-Global Instance persistent_separable P : Persistent P → Separable P | 100.
+Lemma persistently_and_sep_assoc P Q R : <pers> P ∧ (Q ∗ R) ⊣⊢ (<pers> P ∧ Q) ∗ R.
 Proof.
-  rewrite /Persistent /Separable=> HP Q.
-  by rewrite {1}HP absorbingly_elim_persistently persistently_and_sep_elim_emp.
+  apply (anti_symm (⊢)).
+  - rewrite {1}persistently_idemp_2 persistently_and_sep_elim_emp assoc.
+    apply sep_mono_l, and_intro.
+    + by rewrite and_elim_r sep_elim_l.
+    + by rewrite and_elim_l left_id.
+  - apply and_intro.
+    + by rewrite and_elim_l sep_elim_l.
+    + by rewrite and_elim_r.
 Qed.
-
 Lemma persistently_and_emp_elim P : emp ∧ <pers> P ⊢ P.
 Proof. by rewrite comm persistently_and_sep_elim_emp right_id and_elim_r. Qed.
 Lemma persistently_into_absorbingly P : <pers> P ⊢ <absorb> P.
 Proof.
   rewrite -(right_id True%I _ (<pers> _)%I) -{1}(emp_sep True%I).
-  rewrite and_sep_assoc.
+  rewrite persistently_and_sep_assoc.
   rewrite (comm bi_and) persistently_and_emp_elim comm //.
 Qed.
 Lemma persistently_elim P `{!Absorbing P} : <pers> P ⊢ P.
@@ -1191,11 +1012,27 @@ Proof.
   auto using persistently_mono, pure_intro.
 Qed.
 
+Lemma persistently_sep_dup P : <pers> P ⊣⊢ <pers> P ∗ <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 sep_elim_l.
+Qed.
+
+Lemma persistently_and_sep_l_1 P Q : <pers> P ∧ Q ⊢ <pers> P ∗ Q.
+Proof.
+  by rewrite -{1}(emp_sep Q) persistently_and_sep_assoc and_elim_l.
+Qed.
+Lemma persistently_and_sep_r_1 P Q : P ∧ <pers> Q ⊢ P ∗ <pers> Q.
+Proof. by rewrite !(comm _ P) persistently_and_sep_l_1. Qed.
+
 Lemma persistently_and_sep P Q : <pers> (P ∧ Q) ⊢ <pers> (P ∗ Q).
 Proof.
   rewrite persistently_and.
   rewrite -{1}persistently_idemp -persistently_and -{1}(emp_sep Q).
-  by rewrite and_sep_assoc (comm bi_and) persistently_and_emp_elim.
+  by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim.
 Qed.
 
 Lemma persistently_affinely_elim P : <pers> <affine> P ⊣⊢ <pers> P.
@@ -1204,15 +1041,22 @@ Proof.
              persistently_pure left_id.
 Qed.
 
+Lemma and_sep_persistently P Q : <pers> P ∧ <pers> Q ⊣⊢ <pers> P ∗ <pers> Q.
+Proof.
+  apply (anti_symm _); auto using persistently_and_sep_l_1.
+  apply and_intro.
+  - by rewrite sep_elim_l.
+  - by rewrite sep_elim_r.
+Qed.
 Lemma persistently_sep_2 P Q : <pers> P ∗ <pers> Q ⊢ <pers> (P ∗ Q).
 Proof.
-  by rewrite -persistently_and_sep persistently_and -and_sep.
+  by rewrite -persistently_and_sep persistently_and -and_sep_persistently.
 Qed.
 Lemma persistently_sep `{!BiPositive PROP} P Q :
   <pers> (P ∗ Q) ⊣⊢ <pers> P ∗ <pers> Q.
 Proof.
   apply (anti_symm _); auto using persistently_sep_2.
-  rewrite -persistently_affinely_elim affinely_sep -and_sep.
+  rewrite -persistently_affinely_elim affinely_sep -and_sep_persistently.
   apply and_intro.
   - by rewrite (affinely_elim_emp Q) right_id affinely_elim.
   - by rewrite (affinely_elim_emp P) left_id affinely_elim.
@@ -1236,24 +1080,47 @@ Qed.
 Lemma persistently_wand P Q : <pers> (P -∗ Q) ⊢ <pers> P -∗ <pers> Q.
 Proof. apply wand_intro_r. by rewrite persistently_sep_2 wand_elim_l. Qed.
 
+Lemma persistently_entails_l P Q : (P ⊢ <pers> Q) → P ⊢ <pers> Q ∗ P.
+Proof. intros; rewrite -persistently_and_sep_l_1; auto. Qed.
+Lemma persistently_entails_r P Q : (P ⊢ <pers> Q) → P ⊢ P ∗ <pers> Q.
+Proof. intros; rewrite -persistently_and_sep_r_1; auto. Qed.
+
 Lemma persistently_impl_wand_2 P Q : <pers> (P -∗ Q) ⊢ <pers> (P → Q).
 Proof.
   apply persistently_intro', impl_intro_r.
-  rewrite -{2}(emp_sep P) and_sep_assoc.
+  rewrite -{2}(emp_sep P) persistently_and_sep_assoc.
   by rewrite (comm bi_and) persistently_and_emp_elim wand_elim_l.
 Qed.
 
+Lemma impl_wand_persistently_2 P Q : (<pers> P -∗ Q) ⊢ (<pers> P → Q).
+Proof. apply impl_intro_l. by rewrite persistently_and_sep_l_1 wand_elim_r. Qed.
+
 Section persistently_affine_bi.
   Context `{!BiAffine PROP}.
 
   Lemma persistently_emp : <pers> emp ⊣⊢ emp.
   Proof. by rewrite -!True_emp persistently_pure. Qed.
 
+  Lemma persistently_and_sep_l P Q : <pers> P ∧ Q ⊣⊢ <pers> P ∗ Q.
+  Proof.
+    apply (anti_symm (⊢));
+      eauto using persistently_and_sep_l_1, sep_and with typeclass_instances.
+  Qed.
+  Lemma persistently_and_sep_r P Q : P ∧ <pers> Q ⊣⊢ P ∗ <pers> Q.
+  Proof. by rewrite !(comm _ P) persistently_and_sep_l. Qed.
+
   Lemma persistently_impl_wand P Q : <pers> (P → Q) ⊣⊢ <pers> (P -∗ Q).
   Proof.
     apply (anti_symm (⊢)); auto using persistently_impl_wand_2.
     apply persistently_intro', wand_intro_l.
-    by rewrite -and_sep_r persistently_elim impl_elim_r.
+    by rewrite -persistently_and_sep_r persistently_elim impl_elim_r.
+  Qed.
+
+  Lemma impl_wand_persistently P Q : (<pers> P → Q) ⊣⊢ (<pers> P -∗ Q).
+  Proof.
+    apply (anti_symm (⊢)).
+    - by rewrite -impl_wand_1.
+    - apply impl_wand_persistently_2.
   Qed.
 
   Lemma wand_alt P Q : (P -∗ Q) ⊣⊢ ∃ R, R ∗ <pers> (P ∗ R → Q).
@@ -1264,7 +1131,7 @@ Section persistently_affine_bi.
       apply persistently_intro', impl_intro_l.
       by rewrite wand_elim_r persistently_pure right_id.
     - apply exist_elim=> R. apply wand_intro_l.
-      rewrite assoc -and_sep_r.
+      rewrite assoc -persistently_and_sep_r.
       by rewrite persistently_elim impl_elim_r.
   Qed.
 End persistently_affine_bi.
@@ -1272,45 +1139,39 @@ End persistently_affine_bi.
 (* Persistence instances *)
 Global Instance pure_persistent φ : Persistent (PROP:=PROP) ⌜φ⌝.
 Proof. by rewrite /Persistent persistently_pure. Qed.
-Global Hint Cut [_* persistent_separable pure_persistent] : typeclass_instances.
 Global Instance emp_persistent : Persistent (PROP:=PROP) emp.
 Proof. rewrite /Persistent. apply persistently_emp_intro. Qed.
-Global Hint Cut [_* persistent_separable emp_persistent] : typeclass_instances.
 Global Instance and_persistent P Q :
   Persistent P → Persistent Q → Persistent (P ∧ Q).
 Proof. intros. by rewrite /Persistent persistently_and -!persistent. Qed.
-Global Hint Cut [_* persistent_separable and_persistent] : typeclass_instances.
 Global Instance or_persistent P Q :
   Persistent P → Persistent Q → Persistent (P ∨ Q).
 Proof. intros. by rewrite /Persistent persistently_or -!persistent. Qed.
-Global Hint Cut [_* persistent_separable or_persistent] : typeclass_instances.
 Global Instance forall_persistent `{!BiPersistentlyForall PROP} {A} (Ψ : A → PROP) :
   (∀ x, Persistent (Ψ x)) → Persistent (∀ x, Ψ x).
 Proof.
   intros. rewrite /Persistent persistently_forall.
   apply forall_mono=> x. by rewrite -!persistent.
 Qed.
-(** No [Hint Cut] because [Separable] is not closed under [∀]. *)
 Global Instance exist_persistent {A} (Ψ : A → PROP) :
   (∀ x, Persistent (Ψ x)) → Persistent (∃ x, Ψ x).
 Proof.
   intros. rewrite /Persistent persistently_exist.
   apply exist_mono=> x. by rewrite -!persistent.
 Qed.
-Global Hint Cut [_* persistent_separable exist_persistent] : typeclass_instances.
+
 Global Instance sep_persistent P Q :
   Persistent P → Persistent Q → Persistent (P ∗ Q).
 Proof. intros. by rewrite /Persistent -persistently_sep_2 -!persistent. Qed.
+
 Global Instance affinely_persistent P : Persistent P → Persistent (<affine> P).
 Proof. rewrite /bi_affinely. apply _. Qed.
-Global Hint Cut [_* persistent_separable affinely_persistent] : typeclass_instances.
+
 Global Instance absorbingly_persistent P : Persistent P → Persistent (<absorb> P).
 Proof. rewrite /bi_absorbingly. apply _. Qed.
-Global Hint Cut [_* persistent_separable absorbingly_persistent] : typeclass_instances.
 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.
-Global Hint Cut [_* persistent_separable from_option_persistent] : typeclass_instances.
 
 (* The intuitionistic modality *)
 Global Instance intuitionistically_ne : NonExpansive (@bi_intuitionistically PROP).
@@ -1396,9 +1257,16 @@ Lemma intuitionistically_affinely_elim P : □ <affine> P ⊣⊢ □ P.
 Proof. rewrite /bi_intuitionistically persistently_affinely_elim //. Qed.
 
 Lemma persistently_and_intuitionistically_sep_l P Q : <pers> P ∧ Q ⊣⊢ □ P ∗ Q.
-Proof. apply: and_affinely_sep_l. Qed.
+Proof.
+  rewrite /bi_intuitionistically. apply (anti_symm _).
+  - by rewrite /bi_affinely -(comm bi_and (<pers> P)%I)
+      -persistently_and_sep_assoc left_id.
+  - apply and_intro.
+    + by rewrite affinely_elim sep_elim_l.
+    + by rewrite affinely_elim_emp left_id.
+Qed.
 Lemma persistently_and_intuitionistically_sep_r P Q : P ∧ <pers> Q ⊣⊢ P ∗ □ Q.
-Proof. apply: and_affinely_sep_r. Qed.
+Proof. by rewrite !(comm _ P) persistently_and_intuitionistically_sep_l. Qed.
 Lemma and_sep_intuitionistically P Q : □ P ∧ □ Q ⊣⊢ □ P ∗ □ Q.
 Proof.
   rewrite -persistently_and_intuitionistically_sep_l.
@@ -1411,7 +1279,13 @@ Proof.
 Qed.
 
 Lemma impl_wand_intuitionistically P Q : (<pers> P → Q) ⊣⊢ (□ P -∗ Q).
-Proof. apply: impl_affinely_wand. Qed.
+Proof.
+  apply (anti_symm (⊢)).
+  - apply wand_intro_l.
+    by rewrite -persistently_and_intuitionistically_sep_l impl_elim_r.
+  - apply impl_intro_l.
+    by rewrite persistently_and_intuitionistically_sep_l wand_elim_r.
+Qed.
 
 Lemma intuitionistically_alt_fixpoint P :
   □ P ⊣⊢ emp ∧ (P ∗ □ P).
@@ -1670,10 +1544,91 @@ Qed.
 
 Lemma persistently_intro P Q `{!Persistent P} : (P ⊢ Q) → P ⊢ <pers> Q.
 Proof. intros HP. by rewrite (persistent P) HP. Qed.
+Lemma persistent_and_affinely_sep_l_1 P Q `{!Persistent P} :
+  P ∧ Q ⊢ <affine> P ∗ Q.
+Proof.
+  rewrite {1}(persistent_persistently_2 P).
+  rewrite persistently_and_intuitionistically_sep_l.
+  rewrite intuitionistically_affinely //.
+Qed.
+Lemma persistent_and_affinely_sep_r_1 P Q `{!Persistent Q} :
+  P ∧ Q ⊢ P ∗ <affine> Q.
+Proof. by rewrite !(comm _ P) persistent_and_affinely_sep_l_1. Qed.
+
+Lemma persistent_and_affinely_sep_l P Q `{!Persistent P, !Absorbing P} :
+  P ∧ Q ⊣⊢ <affine> P ∗ Q.
+Proof.
+  rewrite -(persistent_persistently P).
+  by rewrite persistently_and_intuitionistically_sep_l.
+Qed.
+Lemma persistent_and_affinely_sep_r P Q `{!Persistent Q, !Absorbing Q} :
+  P ∧ Q ⊣⊢ P ∗ <affine> Q.
+Proof.
+  rewrite -(persistent_persistently Q).
+  by rewrite persistently_and_intuitionistically_sep_r.
+Qed.
+
+Lemma persistent_and_sep_1 P Q `{HPQ : !TCOr (Persistent P) (Persistent Q)} :
+  P ∧ Q ⊢ P ∗ Q.
+Proof.
+  destruct HPQ.
+  - by rewrite persistent_and_affinely_sep_l_1 affinely_elim.
+  - by rewrite persistent_and_affinely_sep_r_1 affinely_elim.
+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.
+Lemma persistent_entails_r P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
+Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
 
 Lemma absorbingly_intuitionistically_into_persistently P :
   <absorb> □ P ⊣⊢ <pers> P.
-Proof. apply: absorbingly_affinely. Qed.
+Proof.
+  apply (anti_symm _).
+  - rewrite intuitionistically_into_persistently_1.
+    by rewrite absorbingly_elim_persistently.
+  - rewrite -{1}(idemp bi_and (<pers> _)%I).
+    rewrite persistently_and_intuitionistically_sep_r.
+    by rewrite {1} (True_intro (<pers> _)%I).
+Qed.
+
+Lemma persistent_absorbingly_affinely_2 P `{!Persistent P} :
+  P ⊢ <absorb> <affine> P.
+Proof.
+  rewrite {1}(persistent P) -absorbingly_intuitionistically_into_persistently.
+  by rewrite intuitionistically_affinely.
+Qed.
+Lemma persistent_absorbingly_affinely P `{!Persistent P, !Absorbing P} :
+  <absorb> <affine> P ⊣⊢ P.
+Proof.
+  rewrite -(persistent_persistently P).
+  by rewrite absorbingly_intuitionistically_into_persistently.
+Qed.
+
+Lemma persistent_and_sep_assoc P `{!Persistent P, !Absorbing P} Q R :
+  P ∧ (Q ∗ R) ⊣⊢ (P ∧ Q) ∗ R.
+Proof. by rewrite -(persistent_persistently P) persistently_and_sep_assoc. Qed.
+Lemma persistent_impl_wand_affinely P `{!Persistent P, !Absorbing P} Q :
+  (P → Q) ⊣⊢ (<affine> P -∗ Q).
+Proof.
+  apply (anti_symm _).
+  - apply wand_intro_l. rewrite -persistent_and_affinely_sep_l impl_elim_r //.
+  - apply impl_intro_l. rewrite persistent_and_affinely_sep_l wand_elim_r //.
+Qed.
+
+Lemma impl_wand_2 P `{!Persistent P} Q : (P -∗ Q) ⊢ P → Q.
+Proof. apply impl_intro_l. by rewrite persistent_and_sep_1 wand_elim_r. Qed.
 
 (** We don't have a [Intuitionistic] typeclass, but if we did, this
 would be its only field. *)
@@ -1683,6 +1638,29 @@ Proof. rewrite intuitionistic_intuitionistically. done. Qed.
 Lemma intuitionistically_intro P Q `{!Affine P, !Persistent P} : (P ⊢ Q) → P ⊢ □ Q.
 Proof. intros. apply: affinely_intro. by apply: persistently_intro. Qed.
 
+Section persistent_bi_absorbing.
+  Context `{!BiAffine PROP}.
+
+  Lemma persistent_and_sep P Q `{HPQ : !TCOr (Persistent P) (Persistent Q)} :
+    P ∧ Q ⊣⊢ P ∗ Q.
+  Proof.
+    destruct HPQ.
+    - by rewrite -(persistent_persistently P) persistently_and_sep_l.
+    - by rewrite -(persistent_persistently Q) persistently_and_sep_r.
+  Qed.
+
+  Lemma impl_wand P `{!Persistent P} Q : (P → Q) ⊣⊢ (P -∗ Q).
+  Proof. apply (anti_symm _); auto using impl_wand_1, impl_wand_2. Qed.
+End persistent_bi_absorbing.
+
+Global Instance impl_absorbing P Q :
+  Persistent P → Absorbing P → Absorbing Q → Absorbing (P → Q).
+Proof.
+  intros. rewrite /Absorbing. apply impl_intro_l.
+  rewrite persistent_and_affinely_sep_l_1 absorbingly_sep_r.
+  by rewrite -persistent_and_affinely_sep_l impl_elim_r.
+Qed.
+
 (* For big ops *)
 Global Instance bi_and_monoid : Monoid (@bi_and PROP) :=
   {| monoid_unit := True%I |}.
diff --git a/iris/bi/derived_laws_later.v b/iris/bi/derived_laws_later.v
index fff6581fd6f1447ccd86ac9246af6ed734f6e6dc..d89ef824376e443981197beb48803f79876a9b36 100644
--- a/iris/bi/derived_laws_later.v
+++ b/iris/bi/derived_laws_later.v
@@ -273,7 +273,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 -sep_dup.
+    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.
@@ -369,7 +369,7 @@ Proof.
   apply or_mono, wand_intro_l; first done.
   rewrite -{2}(löb Q); apply impl_intro_l.
   rewrite HQ /bi_except_0 !and_or_r. apply or_elim; last auto.
-  by rewrite (comm _ P) and_sep_assoc impl_elim_r wand_elim_l.
+  by rewrite (comm _ P) persistent_and_sep_assoc impl_elim_r wand_elim_l.
 Qed.
 Global Instance forall_timeless {A} (Ψ : A → PROP) :
   (∀ x, Timeless (Ψ x)) → Timeless (∀ x, Ψ x).
diff --git a/iris/bi/internal_eq.v b/iris/bi/internal_eq.v
index 56b0f13fdc61caebbdde49c1fdefed6f04277b74..796aa71d55d5fdda77133a7b32ae1d47455a6d7e 100644
--- a/iris/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -229,17 +229,6 @@ Section internal_eq_derived.
   Global Instance internal_eq_persistent {A : ofe} (a b : A) :
     Persistent (PROP:=PROP) (a ≡ b).
   Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.
-  Global Hint Cut [persistent_separable internal_eq_persistent] : typeclasses_instances.
-
-  Global Instance internal_eq_separable {A : ofe} (a b : A) :
-    Separable (PROP:=PROP) (a ≡ b).
-  Proof.
-    intros Q. rewrite absorbingly_internal_eq.
-    apply (internal_eq_rewrite' a b (λ b', <affine> (a ≡ b') ∗ Q)%I); auto.
-    rewrite and_elim_r -(equiv_internal_eq True) //.
-    by rewrite affinely_True_emp left_id.
-  Qed.
-  (* Hint Cut [plain_separable internal_eq_plain] is in [bi.plainly] *)
 
   (* Equality under a later. *)
   Lemma internal_eq_rewrite_contractive {A : ofe} a b (Ψ : A → PROP)
diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index b8d3de822c60c5834fbfe5fd5f4feb50b3343526..6b985d9ecc7902dd0c40f50544bf7e190472a81b 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -71,7 +71,7 @@ Section fractional.
   (** Fractional and logical connectives *)
   Global Instance persistent_fractional (P : PROP) :
     Persistent P → TCOr (Affine P) (Absorbing P) → Fractional (λ _, P).
-  Proof. intros ?? q q'. apply: bi.sep_dup. Qed.
+  Proof. intros ?? q q'. apply: bi.persistent_sep_dup. Qed.
 
   (** We do not have [AsFractional] instances for [∗] and the big operators
   because the [iDestruct] tactic already turns [P ∗ Q] into [P] and [Q],
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index b55cbb110568f0bd452ec0a25b8aa5c96260b1a5..3f87dbfc3a7f7015d7b0384899fc96841cc98ef1 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -134,19 +134,6 @@ Section plainly_derived.
     Proper (flip (⊢) ==> flip (⊢)) (@plainly PROP _).
   Proof. intros P Q; apply plainly_mono. Qed.
 
-  (* Not an instance; registered as [Hint Immediate] at the bottom of this file *)
-  Lemma plain_persistent P : Plain P → Persistent P.
-  Proof. intros. by rewrite /Persistent -plainly_elim_persistently. Qed.
-
-  (** High cost, should only be used if no other [Separable] instances can be
-  applied *)
-  (** FIXME: Remove once [plain_persistent] is no longer [Hint Immediate]. *)
-  Global Instance plain_separable P : Plain P → Separable P | 100.
-  Proof. intros. by apply persistent_separable, plain_persistent. Qed.
-
-  Global Instance plainly_absorbing P : Absorbing (â–  P).
-  Proof. by rewrite /Absorbing /bi_absorbingly comm plainly_absorb. Qed.
-
   Lemma affinely_plainly_elim P : <affine> ■ P ⊢ P.
   Proof. by rewrite plainly_elim_persistently /bi_affinely persistently_and_emp_elim. Qed.
 
@@ -173,6 +160,8 @@ Section plainly_derived.
 
   Lemma plainly_and_sep_elim P Q : ■ P ∧ Q ⊢ (emp ∧ P) ∗ Q.
   Proof. by rewrite plainly_elim_persistently persistently_and_sep_elim_emp. Qed.
+  Lemma plainly_and_sep_assoc P Q R : ■ P ∧ (Q ∗ R) ⊣⊢ (■ P ∧ Q) ∗ R.
+  Proof. by rewrite -(persistently_elim_plainly P) persistently_and_sep_assoc. Qed.
   Lemma plainly_and_emp_elim P : emp ∧ ■ P ⊢ P.
   Proof. by rewrite plainly_elim_persistently persistently_and_emp_elim. Qed.
   Lemma plainly_into_absorbingly P : ■ P ⊢ <absorb> P.
@@ -184,8 +173,6 @@ Section plainly_derived.
   Proof. by rewrite plainly_into_absorbingly absorbingly_elim_plainly. Qed.
   Lemma plainly_idemp P : ■ ■ P ⊣⊢ ■ P.
   Proof. apply (anti_symm _); auto using plainly_idemp_1, plainly_idemp_2. Qed.
-  Global Instance plainly_plain P : Plain (â–  P).
-  Proof. by rewrite /Plain plainly_idemp. Qed.
 
   Lemma plainly_intro' P Q : (■ P ⊢ Q) → ■ P ⊢ ■ Q.
   Proof. intros <-. apply plainly_idemp_2. Qed.
@@ -223,13 +210,26 @@ Section plainly_derived.
   Lemma plainly_emp_2 : emp ⊢@{PROP} ■ emp.
   Proof. apply plainly_emp_intro. Qed.
 
+  Lemma plainly_sep_dup P : ■ P ⊣⊢ ■ P ∗ ■ 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.
+  Qed.
+
+  Lemma plainly_and_sep_l_1 P Q : ■ P ∧ Q ⊢ ■ P ∗ Q.
+  Proof. by rewrite -{1}(emp_sep Q) plainly_and_sep_assoc and_elim_l. Qed.
+  Lemma plainly_and_sep_r_1 P Q : P ∧ ■ Q ⊢ P ∗ ■ Q.
+  Proof. by rewrite !(comm _ P) plainly_and_sep_l_1. Qed.
+
   Lemma plainly_True_emp : ■ True ⊣⊢@{PROP} ■ emp.
   Proof. apply (anti_symm _); eauto using plainly_mono, plainly_emp_intro. Qed.
   Lemma plainly_and_sep P Q : ■ (P ∧ Q) ⊢ ■ (P ∗ Q).
   Proof.
     rewrite plainly_and.
     rewrite -{1}plainly_idemp -plainly_and -{1}(emp_sep Q).
-    by rewrite and_sep_assoc (comm bi_and) plainly_and_emp_elim.
+    by rewrite plainly_and_sep_assoc (comm bi_and) plainly_and_emp_elim.
   Qed.
 
   Lemma plainly_affinely_elim P : ■ <affine> P ⊣⊢ ■ P.
@@ -243,12 +243,19 @@ Section plainly_derived.
     rewrite persistently_elim_plainly plainly_persistently_elim. done.
   Qed.
 
+  Lemma and_sep_plainly P Q : ■ P ∧ ■ Q ⊣⊢ ■ P ∗ ■ Q.
+  Proof.
+    apply (anti_symm _); auto using plainly_and_sep_l_1.
+    apply and_intro.
+    - by rewrite plainly_absorb.
+    - by rewrite comm plainly_absorb.
+  Qed.
   Lemma plainly_sep_2 P Q : ■ P ∗ ■ Q ⊢ ■ (P ∗ Q).
-  Proof. by rewrite -plainly_and_sep plainly_and -and_sep. Qed.
+  Proof. by rewrite -plainly_and_sep plainly_and -and_sep_plainly. Qed.
   Lemma plainly_sep `{!BiPositive PROP} P Q : ■ (P ∗ Q) ⊣⊢ ■ P ∗ ■ Q.
   Proof.
     apply (anti_symm _); auto using plainly_sep_2.
-    rewrite -(plainly_affinely_elim (_ ∗ _)) affinely_sep -and_sep. apply and_intro.
+    rewrite -(plainly_affinely_elim (_ ∗ _)) affinely_sep -and_sep_plainly. apply and_intro.
     - by rewrite (affinely_elim_emp Q) right_id affinely_elim.
     - by rewrite (affinely_elim_emp P) left_id affinely_elim.
   Qed.
@@ -256,20 +263,31 @@ Section plainly_derived.
   Lemma plainly_wand P Q : ■ (P -∗ Q) ⊢ ■ P -∗ ■ Q.
   Proof. apply wand_intro_r. by rewrite plainly_sep_2 wand_elim_l. Qed.
 
+  Lemma plainly_entails_l P Q : (P ⊢ ■ Q) → P ⊢ ■ Q ∗ P.
+  Proof. intros; rewrite -plainly_and_sep_l_1; auto. Qed.
+  Lemma plainly_entails_r P Q : (P ⊢ ■ Q) → P ⊢ P ∗ ■ Q.
+  Proof. intros; rewrite -plainly_and_sep_r_1; auto. Qed.
+
   Lemma plainly_impl_wand_2 P Q : ■ (P -∗ Q) ⊢ ■ (P → Q).
   Proof.
     apply plainly_intro', impl_intro_r.
-    rewrite -{2}(emp_sep P) and_sep_assoc.
+    rewrite -{2}(emp_sep P) plainly_and_sep_assoc.
     by rewrite (comm bi_and) plainly_and_emp_elim wand_elim_l.
   Qed.
 
+  Lemma impl_wand_plainly_2 P Q : (■ P -∗ Q) ⊢ (■ P → Q).
+  Proof. apply impl_intro_l. by rewrite plainly_and_sep_l_1 wand_elim_r. Qed.
+
+  Lemma impl_wand_affinely_plainly P Q : (■ P → Q) ⊣⊢ (<affine> ■ P -∗ Q).
+  Proof. by rewrite -(persistently_elim_plainly P) impl_wand_intuitionistically. Qed.
+
   Lemma persistently_wand_affinely_plainly `{!BiPersistentlyImplPlainly PROP} P Q :
     (<affine> ■ P -∗ <pers> Q) ⊢ <pers> (<affine> ■ P -∗ Q).
-  Proof. rewrite -!impl_affinely_wand. apply: persistently_impl_plainly. Qed.
+  Proof. rewrite -!impl_wand_affinely_plainly. apply: persistently_impl_plainly. Qed.
 
   Lemma plainly_wand_affinely_plainly P Q :
     (<affine> ■ P -∗ ■ Q) ⊢ ■ (<affine> ■ P -∗ Q).
-  Proof. rewrite -!impl_affinely_wand. apply plainly_impl_plainly. Qed.
+  Proof. rewrite -!impl_wand_affinely_plainly. apply plainly_impl_plainly. Qed.
 
   Section plainly_affine_bi.
     Context `{!BiAffine PROP}.
@@ -277,11 +295,26 @@ Section plainly_derived.
     Lemma plainly_emp : ■ emp ⊣⊢@{PROP} emp.
     Proof. by rewrite -!True_emp plainly_pure. Qed.
 
+    Lemma plainly_and_sep_l P Q : ■ P ∧ Q ⊣⊢ ■ P ∗ Q.
+    Proof.
+      apply (anti_symm (⊢));
+        eauto using plainly_and_sep_l_1, sep_and with typeclass_instances.
+    Qed.
+    Lemma plainly_and_sep_r P Q : P ∧ ■ Q ⊣⊢ P ∗ ■ Q.
+    Proof. by rewrite !(comm _ P) plainly_and_sep_l. Qed.
+
     Lemma plainly_impl_wand P Q : ■ (P → Q) ⊣⊢ ■ (P -∗ Q).
     Proof.
       apply (anti_symm (⊢)); auto using plainly_impl_wand_2.
       apply plainly_intro', wand_intro_l.
-      by rewrite -and_sep_r plainly_elim impl_elim_r.
+      by rewrite -plainly_and_sep_r plainly_elim impl_elim_r.
+    Qed.
+
+    Lemma impl_wand_plainly P Q : (■ P → Q) ⊣⊢ (■ P -∗ Q).
+    Proof.
+      apply (anti_symm (⊢)).
+      - by rewrite -impl_wand_1.
+      - by rewrite impl_wand_plainly_2.
     Qed.
   End plainly_affine_bi.
 
@@ -330,10 +363,16 @@ Section plainly_derived.
   Proof. by intros <-. Qed.
 
   (* Typeclass instances *)
+  Global Instance plainly_absorbing P : Absorbing (â–  P).
+  Proof. by rewrite /Absorbing /bi_absorbingly comm plainly_absorb. Qed.
   Global Instance plainly_if_absorbing P p :
     Absorbing P → Absorbing (plainly_if p P).
   Proof. intros; destruct p; simpl; apply _. Qed.
 
+  (* Not an instance, see the bottom of this file *)
+  Lemma plain_persistent P : Plain P → Persistent P.
+  Proof. intros. by rewrite /Persistent -plainly_elim_persistently. Qed.
+
   Global Instance impl_persistent `{!BiPersistentlyImplPlainly PROP} P Q :
     Absorbing P → Plain P → Persistent Q → Persistent (P → Q).
   Proof.
@@ -348,7 +387,7 @@ Section plainly_derived.
     Plain P → Persistent Q → Absorbing Q → Persistent (P -∗ Q).
   Proof.
     intros. rewrite /Persistent {2}(plain P). trans (<pers> (■ P → Q))%I.
-    - rewrite -persistently_impl_plainly impl_affinely_wand -(persistent Q).
+    - rewrite -persistently_impl_plainly impl_wand_affinely_plainly -(persistent Q).
       by rewrite affinely_plainly_elim.
     - apply persistently_mono, wand_intro_l. by rewrite sep_and impl_elim_r.
   Qed.
@@ -412,66 +451,54 @@ Section plainly_derived.
   (* Plainness instances *)
   Global Instance pure_plain φ : Plain (PROP:=PROP) ⌜φ⌝.
   Proof. by rewrite /Plain plainly_pure. Qed.
-  Global Hint Cut [_* plain_separable pure_plain] : typeclass_instances.
   Global Instance emp_plain : Plain (PROP:=PROP) emp.
   Proof. apply plainly_emp_intro. Qed.
-  Global Hint Cut [_* plain_separable emp_plain] : typeclass_instances.
   Global Instance and_plain P Q : Plain P → Plain Q → Plain (P ∧ Q).
   Proof. intros. by rewrite /Plain plainly_and -!plain. Qed.
-  Global Hint Cut [_* plain_separable and_plain] : typeclass_instances.
   Global Instance or_plain P Q : Plain P → Plain Q → Plain (P ∨ Q).
   Proof. intros. by rewrite /Plain -plainly_or_2 -!plain. Qed.
-  Global Hint Cut [_* plain_separable or_plain] : typeclass_instances.
   Global Instance forall_plain {A} (Ψ : A → PROP) :
     (∀ x, Plain (Ψ x)) → Plain (∀ x, Ψ x).
   Proof.
     intros. rewrite /Plain plainly_forall. apply forall_mono=> x. by rewrite -plain.
   Qed.
-  (** No [Hint Cut] because [Separable] is not closed under ∀. *)
   Global Instance exist_plain {A} (Ψ : A → PROP) :
     (∀ x, Plain (Ψ x)) → Plain (∃ x, Ψ x).
   Proof.
     intros. rewrite /Plain -plainly_exist_2. apply exist_mono=> x. by rewrite -plain.
   Qed.
-  Global Hint Cut [_* plain_separable exist_plain] : typeclass_instances.
 
   Global Instance impl_plain P Q : Absorbing P → Plain P → Plain Q → Plain (P → Q).
   Proof.
     intros. by rewrite /Plain {2}(plain P) -plainly_impl_plainly -(plain Q)
                        (plainly_into_absorbingly P) absorbing.
   Qed.
-  (** No [Hint Cut] because [Separable] is not closed under [→]. *)
   Global Instance wand_plain P Q :
     Plain P → Plain Q → Absorbing Q → Plain (P -∗ Q).
   Proof.
     intros. rewrite /Plain {2}(plain P). trans (■ (■ P → Q))%I.
-    - rewrite -plainly_impl_plainly impl_affinely_wand -(plain Q).
+    - rewrite -plainly_impl_plainly impl_wand_affinely_plainly -(plain Q).
       by rewrite affinely_plainly_elim.
     - apply plainly_mono, wand_intro_l. by rewrite sep_and impl_elim_r.
   Qed.
-  (** No [Hint Cut] because [Separable] is not closed under [-∗]. *)
   Global Instance sep_plain P Q : Plain P → Plain Q → Plain (P ∗ Q).
   Proof. intros. by rewrite /Plain -plainly_sep_2 -!plain. Qed.
-  Global Hint Cut [_* plain_separable sep_plain] : typeclass_instances.
 
+  Global Instance plainly_plain P : Plain (â–  P).
+  Proof. by rewrite /Plain plainly_idemp. Qed.
   Global Instance persistently_plain P : Plain P → Plain (<pers> P).
   Proof.
     rewrite /Plain=> HP. rewrite {1}HP plainly_persistently_elim persistently_elim_plainly //.
   Qed.
-  Global Hint Cut [_* plain_separable persistently_plain] : typeclass_instances.
   Global Instance affinely_plain P : Plain P → Plain (<affine> P).
   Proof. rewrite /bi_affinely. apply _. Qed.
-  Global Hint Cut [_* plain_separable affinely_plain] : typeclass_instances.
   Global Instance intuitionistically_plain P : Plain P → Plain (□ P).
   Proof. rewrite /bi_intuitionistically. apply _. Qed.
-  Global Hint Cut [_* plain_separable intuitionistically_plain] : typeclass_instances.
   Global Instance absorbingly_plain P : Plain P → Plain (<absorb> P).
   Proof. rewrite /bi_absorbingly. apply _. Qed.
-  Global Hint Cut [_* plain_separable absorbingly_plain] : typeclass_instances.
   Global Instance from_option_plain {A} P (Ψ : A → PROP) (mx : option A) :
     (∀ x, Plain (Ψ x)) → Plain P → Plain (from_option Ψ P mx).
   Proof. destruct mx; apply _. Qed.
-  Global Hint Cut [_* plain_separable from_option_plain] : typeclass_instances.
 
   Global Instance big_sepL_nil_plain `{!BiAffine PROP} {A} (Φ : nat → A → PROP) :
     Plain ([∗ list] k↦x ∈ [], Φ k x).
@@ -561,7 +588,6 @@ Section plainly_derived.
     Global Instance internal_eq_plain {A : ofe} (a b : A) :
       Plain (PROP:=PROP) (a ≡ b).
     Proof. by intros; rewrite /Plain plainly_internal_eq. Qed.
-    Global Hint Cut [plain_separable internal_eq_plain] : typeclass_instances.
   End internal_eq.
 
   Section prop_ext.
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index fa991df734628eb2e954763113907f9c3b43e85a..ade5e63773b5ee6a51c0bddf63da442b8038a937 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -442,7 +442,7 @@ Section fupd_derived.
   Lemma big_sepL2_fupd {A B} E (Φ : nat → A → B → PROP) l1 l2 :
     ([∗ list] k↦x;y ∈ l1;l2, |={E}=> Φ k x y) ⊢ |={E}=> [∗ list] k↦x;y ∈ l1;l2, Φ k x y.
   Proof.
-    rewrite !big_sepL2_alt !and_affinely_sep_l.
+    rewrite !big_sepL2_alt !persistent_and_affinely_sep_l.
     etrans; [| by apply fupd_frame_l]. apply sep_mono_r. apply big_sepL_fupd.
   Qed.
 
diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index 20d812ef4234eac92e43bf167865b8328eb4d7b9..765cd82abfa9c080cb0536ac705e92e16feeaeed 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -282,8 +282,8 @@ Global Instance from_pure_pure_sep_true a1 a2 (φ1 φ2 : Prop) P1 P2 :
   FromPure (if a1 then a2 else false) (P1 ∗ P2) (φ1 ∧ φ2).
 Proof.
   rewrite /FromPure=> <- <-. destruct a1; simpl.
-  - by rewrite pure_and -and_affinely_sep_l affinely_if_and_r.
-  - by rewrite pure_and -affinely_affinely_if -and_affinely_sep_r_1.
+  - by rewrite pure_and -persistent_and_affinely_sep_l affinely_if_and_r.
+  - by rewrite pure_and -affinely_affinely_if -persistent_and_affinely_sep_r_1.
 Qed.
 Global Instance from_pure_pure_wand a (φ1 φ2 : Prop) P1 P2 :
   IntoPure P1 φ1 → FromPure a P2 φ2 →
@@ -293,7 +293,7 @@ Proof.
   rewrite /FromPure /IntoPure=> HP1 <- Ha /=. apply wand_intro_l.
   destruct a; simpl.
   - destruct Ha as [Ha|?]; first inversion Ha.
-    rewrite -and_affinely_sep_r -(affine_affinely P1) HP1.
+    rewrite -persistent_and_affinely_sep_r -(affine_affinely P1) HP1.
     by rewrite affinely_and_l pure_impl_1 impl_elim_r.
   - by rewrite HP1 sep_and pure_impl_1 impl_elim_r.
 Qed.
@@ -318,7 +318,7 @@ Global Instance from_pure_absorbingly a P φ :
   FromPure a P φ → FromPure false (<absorb> P) φ.
 Proof.
   rewrite /FromPure=> <- /=. rewrite -affinely_affinely_if.
-  by rewrite -absorbingly_affinely_2.
+  by rewrite -persistent_absorbingly_affinely_2.
 Qed.
 
 Global Instance from_pure_big_sepL {A}
@@ -449,7 +449,7 @@ Proof.
   rewrite /MakeAffinely /IntoWand /FromAssumption /= => ? Hpers <- ->.
   apply wand_intro_l. destruct Hpers.
   - rewrite impl_wand_1 affinely_elim wand_elim_r //.
-  - rewrite impl_affinely_wand wand_elim_r //.
+  - rewrite persistent_impl_wand_affinely wand_elim_r //.
 Qed.
 Global Instance into_wand_impl_false_true P Q P' :
   Absorbing P' →
@@ -458,7 +458,7 @@ Global Instance into_wand_impl_false_true P Q P' :
 Proof.
   rewrite /IntoWand /FromAssumption /= => ? HP. apply wand_intro_l.
   rewrite -(persistently_elim P').
-  rewrite impl_affinely_wand.
+  rewrite persistent_impl_wand_affinely.
   rewrite -(intuitionistically_idemp P) HP.
   apply wand_elim_r.
 Qed.
@@ -503,7 +503,7 @@ Global Instance into_wand_forall_prop_false p (φ : Prop) Pφ P :
 Proof.
   rewrite /MakeAffinely /IntoWand=> <-.
   rewrite (intuitionistically_if_elim p) /=.
-  by rewrite -pure_impl_forall -impl_affinely_wand.
+  by rewrite -pure_impl_forall -persistent_impl_wand_affinely.
 Qed.
 
 Global Instance into_wand_forall {A} p q (Φ : A → PROP) P Q x :
@@ -573,14 +573,14 @@ Global Instance from_and_sep_persistent_l P1 P1' P2 :
   Persistent P1 → IntoAbsorbingly P1' P1 → FromAnd (P1 ∗ P2) P1' P2 | 9.
 Proof.
   rewrite /IntoAbsorbingly /FromAnd=> ? ->.
-  rewrite and_affinely_sep_l_1 {1}(persistent_persistently_2 P1).
+  rewrite persistent_and_affinely_sep_l_1 {1}(persistent_persistently_2 P1).
   by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P1).
 Qed.
 Global Instance from_and_sep_persistent_r P1 P2 P2' :
   Persistent P2 → IntoAbsorbingly P2' P2 → FromAnd (P1 ∗ P2) P1 P2' | 10.
 Proof.
   rewrite /IntoAbsorbingly /FromAnd=> ? ->.
-  rewrite and_affinely_sep_r_1 {1}(persistent_persistently_2 P2).
+  rewrite persistent_and_affinely_sep_r_1 {1}(persistent_persistently_2 P2).
   by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P2).
 Qed.
 
@@ -600,13 +600,13 @@ Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat → A → PROP)
   IsCons l x l' →
   Persistent (Φ 0 x) →
   FromAnd ([∗ list] k ↦ y ∈ l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l', Φ (S k) y).
-Proof. rewrite /IsCons=> -> ?. by rewrite /FromAnd big_sepL_cons and_sep_1. Qed.
+Proof. rewrite /IsCons=> -> ?. by rewrite /FromAnd big_sepL_cons persistent_and_sep_1. Qed.
 Global Instance from_and_big_sepL_app_persistent {A} (Φ : nat → A → PROP) l l1 l2 :
   IsApp l l1 l2 →
   (∀ k y, Persistent (Φ k y)) →
   FromAnd ([∗ list] k ↦ y ∈ l, Φ k y)
     ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
-Proof. rewrite /IsApp=> -> ?. by rewrite /FromAnd big_sepL_app and_sep_1. Qed.
+Proof. rewrite /IsApp=> -> ?. by rewrite /FromAnd big_sepL_app persistent_and_sep_1. Qed.
 
 Global Instance from_and_big_sepL2_cons_persistent {A B}
     (Φ : nat → A → B → PROP) l1 x1 l1' l2 x2 l2' :
@@ -616,7 +616,7 @@ Global Instance from_and_big_sepL2_cons_persistent {A B}
     (Φ 0 x1 x2) ([∗ list] k ↦ y1;y2 ∈ l1';l2', Φ (S k) y1 y2).
 Proof.
   rewrite /IsCons=> -> -> ?.
-  by rewrite /FromAnd big_sepL2_cons and_sep_1.
+  by rewrite /FromAnd big_sepL2_cons persistent_and_sep_1.
 Qed.
 Global Instance from_and_big_sepL2_app_persistent {A B}
     (Φ : nat → A → B → PROP) l1 l1' l1'' l2 l2' l2'' :
@@ -626,7 +626,7 @@ Global Instance from_and_big_sepL2_app_persistent {A B}
     ([∗ list] k ↦ y1;y2 ∈ l1';l2', Φ k y1 y2)
     ([∗ list] k ↦ y1;y2 ∈ l1'';l2'', Φ (length l1' + k) y1 y2).
 Proof.
-  rewrite /IsApp=> -> -> ?. rewrite /FromAnd and_sep_1.
+  rewrite /IsApp=> -> -> ?. rewrite /FromAnd persistent_and_sep_1.
   apply wand_elim_l', big_sepL2_app.
 Qed.
 
@@ -634,7 +634,7 @@ Global Instance from_and_big_sepMS_disj_union_persistent
     `{Countable A} (Φ : A → PROP) X1 X2 :
   (∀ y, Persistent (Φ y)) →
   FromAnd ([∗ mset] y ∈ X1 ⊎ X2, Φ y) ([∗ mset] y ∈ X1, Φ y) ([∗ mset] y ∈ X2, Φ y).
-Proof. intros. by rewrite /FromAnd big_sepMS_disj_union and_sep_1. Qed.
+Proof. intros. by rewrite /FromAnd big_sepMS_disj_union persistent_and_sep_1. Qed.
 
 (** FromSep *)
 Global Instance from_sep_sep P1 P2 : FromSep (P1 ∗ P2) P1 P2 | 100.
@@ -804,20 +804,20 @@ Global Instance into_sep_and_persistent_l P P' Q Q' :
 Proof.
   destruct 2 as [P Q Q'|P Q]; rewrite /IntoSep.
   - rewrite -(from_affinely Q' Q) -(affine_affinely P) affinely_and_lr.
-    by rewrite and_affinely_sep_l_1.
-  - by rewrite and_affinely_sep_l_1.
+    by rewrite persistent_and_affinely_sep_l_1.
+  - by rewrite persistent_and_affinely_sep_l_1.
 Qed.
 Global Instance into_sep_and_persistent_r P P' Q Q' :
   Persistent Q → AndIntoSep Q Q' P P' → IntoSep (P ∧ Q) P' Q'.
 Proof.
   destruct 2 as [Q P P'|Q P]; rewrite /IntoSep.
   - rewrite -(from_affinely P' P) -(affine_affinely Q) -affinely_and_lr.
-    by rewrite and_affinely_sep_r_1.
-  - by rewrite and_affinely_sep_r_1.
+    by rewrite persistent_and_affinely_sep_r_1.
+  - by rewrite persistent_and_affinely_sep_r_1.
 Qed.
 
 Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
-Proof. by rewrite /IntoSep pure_and and_sep_1. Qed.
+Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.
 
 Global Instance into_sep_affinely `{!BiPositive PROP} P Q1 Q2 :
   IntoSep P Q1 Q2 → IntoSep (<affine> P) (<affine> Q1) (<affine> Q2) | 0.
@@ -842,7 +842,7 @@ Global Instance into_sep_persistently_affine P Q1 Q2 :
   IntoSep (<pers> P) (<pers> Q1) (<pers> Q2).
 Proof.
   rewrite /IntoSep /= => -> ??.
-  by rewrite sep_and persistently_and and_sep_l_1.
+  by rewrite sep_and persistently_and persistently_and_sep_l_1.
 Qed.
 Global Instance into_sep_intuitionistically_affine P Q1 Q2 :
   IntoSep P Q1 Q2 →
@@ -1065,7 +1065,7 @@ Global Instance from_forall_wand_pure P Q φ :
   FromForall (P -∗ Q) (λ _ : φ, Q)%I (to_ident_name H).
 Proof.
   intros (φ'&->&?) [|]; rewrite /FromForall; apply wand_intro_r.
-  - rewrite -(affine_affinely P) (into_pure P) -and_affinely_sep_r.
+  - rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_r.
     apply pure_elim_r=>?. by rewrite forall_elim.
   - by rewrite (into_pure P) -pure_wand_forall wand_elim_l.
 Qed.
diff --git a/iris/proofmode/class_instances_frame.v b/iris/proofmode/class_instances_frame.v
index 583e883862915478a09c346e638c295e50ffb6ef..e3c78d51eb4e9a5c49f7c7cfc3e908d52a2d014a 100644
--- a/iris/proofmode/class_instances_frame.v
+++ b/iris/proofmode/class_instances_frame.v
@@ -183,7 +183,7 @@ Global Instance frame_persistently R P Q Q' :
 Proof.
   rewrite /Frame /MakePersistently=> <- <- /=.
   rewrite -persistently_and_intuitionistically_sep_l.
-  by rewrite -persistently_sep_2 -and_sep_l_1
+  by rewrite -persistently_sep_2 -persistently_and_sep_l_1
     persistently_affinely_elim persistently_idemp.
 Qed.
 
diff --git a/iris/proofmode/class_instances_later.v b/iris/proofmode/class_instances_later.v
index 0d14c49f81806a47c15f3d500119c0b403595a78..6ee58f912c64b1c26450a6cb11e61ef0502ccbdc 100644
--- a/iris/proofmode/class_instances_later.v
+++ b/iris/proofmode/class_instances_later.v
@@ -148,7 +148,7 @@ Proof.
   rewrite /IntoSep /= => -> ??.
   rewrite -{1}(affine_affinely Q1) -{1}(affine_affinely Q2) later_sep !later_affinely_1.
   rewrite -except_0_sep /bi_except_0 affinely_or. apply or_elim, affinely_elim.
-  rewrite -(idemp bi_and (<affine> â–· False)%I) and_sep_1.
+  rewrite -(idemp bi_and (<affine> â–· False)%I) persistent_and_sep_1.
   by rewrite -(False_elim Q1) -(False_elim Q2).
 Qed.
 
diff --git a/iris/proofmode/class_instances_plainly.v b/iris/proofmode/class_instances_plainly.v
index 1741cff659586b9d13d99af3f0a66b97edd7d61d..0971f80cd2681716ba5cd883c0631061efb0010f 100644
--- a/iris/proofmode/class_instances_plainly.v
+++ b/iris/proofmode/class_instances_plainly.v
@@ -60,8 +60,7 @@ Global Instance into_sep_plainly_affine P Q1 Q2 :
   TCOr (Affine Q1) (Absorbing Q2) → TCOr (Affine Q2) (Absorbing Q1) →
   IntoSep (â–  P) (â–  Q1) (â–  Q2).
 Proof.
-  rewrite /IntoSep /= => -> ??.
-  by rewrite sep_and plainly_and and_sep_l_1.
+  rewrite /IntoSep /= => -> ??. by rewrite sep_and plainly_and plainly_and_sep_l_1.
 Qed.
 
 Global Instance from_or_plainly P Q1 Q2 :
diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index 8c4495fdcb557527b6d0a98ef04914dd050e69aa..06b7f5690b237b6d4646c9b8709273676a83ea01 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -36,7 +36,7 @@ Proof.
   cbv zeta. destruct (env_spatial Δ).
   - rewrite env_to_prop_and_pers_sound. rewrite comm. done.
   - rewrite env_to_prop_and_pers_sound env_to_prop_sound.
-    rewrite /bi_affinely [(emp ∧ _)%I]comm -and_sep_assoc left_id //.
+    rewrite /bi_affinely [(emp ∧ _)%I]comm -persistent_and_sep_assoc left_id //.
 Qed.
 
 (** * Basic rules *)
@@ -168,10 +168,10 @@ Proof.
   - rewrite (into_pure P) -persistently_and_intuitionistically_sep_l persistently_pure.
     by apply pure_elim_l.
   - destruct HPQ.
-    + rewrite -(affine_affinely P) (into_pure P) -and_affinely_sep_l.
+    + rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
       by apply pure_elim_l.
-    + rewrite (into_pure P) -(absorbingly_affinely ⌜ _ ⌝) absorbingly_sep_lr.
-      rewrite -and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
+    + rewrite (into_pure P) -(persistent_absorbingly_affinely ⌜ _ ⌝) absorbingly_sep_lr.
+      rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
 Qed.
 
 Lemma tac_pure_revert Δ φ P Q :
@@ -240,7 +240,7 @@ Proof.
     rewrite -(from_affinely P' P) -affinely_and_lr.
     by rewrite persistently_and_intuitionistically_sep_r intuitionistically_elim wand_elim_r.
   - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
-    by rewrite -(from_affinely P' P) and_affinely_sep_l_1 wand_elim_r.
+    by rewrite -(from_affinely P' P) persistent_and_affinely_sep_l_1 wand_elim_r.
 Qed.
 Lemma tac_impl_intro_intuitionistic Δ i P P' Q R :
   FromImpl R P Q →
@@ -1014,8 +1014,8 @@ Proof.
   rewrite -(idemp bi_and (of_envs Δ)) {2}(envs_lookup_sound _ i) //.
   rewrite (envs_simple_replace_singleton_sound _ _ j) //=.
   rewrite HP HPxy (intuitionistically_if_elim _ (_ ≡ _)) sep_elim_l.
-  rewrite and_affinely_sep_r -assoc. apply wand_elim_r'.
-  rewrite -and_affinely_sep_r. apply impl_elim_r'. destruct d.
+  rewrite persistent_and_affinely_sep_r -assoc. apply wand_elim_r'.
+  rewrite -persistent_and_affinely_sep_r. apply impl_elim_r'. destruct d.
   - apply (internal_eq_rewrite x y (λ y, □?q Φ y -∗ of_envs Δ')%I). solve_proper.
   - rewrite internal_eq_sym.
     eapply (internal_eq_rewrite y x (λ y, □?q Φ y -∗ of_envs Δ')%I). solve_proper.
@@ -1241,7 +1241,7 @@ Section tac_modal_intro.
     trans (<absorb>?fi Q')%I; last first.
     { destruct fi; last done. apply: absorbing. }
     simpl. rewrite -(HQ' Hφ). rewrite -HQ pure_True // left_id. clear HQ' HQ.
-    rewrite !and_affinely_sep_l.
+    rewrite !persistent_and_affinely_sep_l.
     rewrite -modality_sep absorbingly_if_sep. f_equiv.
     - rewrite -absorbingly_if_intro.
       remember (modality_intuitionistic_action M).
@@ -1288,7 +1288,7 @@ Lemma into_laterN_env_sound {PROP : bi} n (Δ1 Δ2 : envs PROP) :
   MaybeIntoLaterNEnvs n Δ1 Δ2 → of_envs Δ1 ⊢ ▷^n (of_envs Δ2).
 Proof.
   intros [[Hp ??] [Hs ??]]; rewrite !of_envs_eq.
-  rewrite ![(env_and_persistently _ ∧ _)%I]and_affinely_sep_l.
+  rewrite ![(env_and_persistently _ ∧ _)%I]persistent_and_affinely_sep_l.
   rewrite !laterN_and !laterN_sep.
   rewrite -{1}laterN_intro. apply and_mono, sep_mono.
   - apply pure_mono; destruct 1; constructor; naive_solver.
diff --git a/iris/proofmode/environments.v b/iris/proofmode/environments.v
index 5ca457c899806208c0aa227dffdb97bb2c3b082f..46a92dbdc1785fafe7e7e1ce1941ad9855ffb930 100644
--- a/iris/proofmode/environments.v
+++ b/iris/proofmode/environments.v
@@ -396,7 +396,7 @@ Lemma of_envs'_alt Γp Γs :
   of_envs' Γp Γs ⊣⊢ ⌜envs_wf' Γp Γs⌝ ∧ □ [∧] Γp ∗ [∗] Γs.
 Proof.
   rewrite /of_envs'. f_equiv.
-  rewrite -and_affinely_sep_l. f_equiv.
+  rewrite -persistent_and_affinely_sep_l. f_equiv.
   clear. induction Γp as [|Γp IH ? Q]; simpl.
   { apply (anti_symm (⊢)); last by apply True_intro.
     by rewrite persistently_True. }
@@ -511,7 +511,7 @@ Proof.
       naive_solver eauto using env_delete_wf, env_delete_fresh).
     rewrite (env_lookup_perm Γs) //=.
     rewrite ![(P ∗ _)%I]comm.
-    rewrite and_sep_assoc. done.
+    rewrite persistent_and_sep_assoc. done.
 Qed.
 Lemma envs_lookup_sound Δ i p P :
   envs_lookup i Δ = Some (p,P) →
@@ -532,7 +532,7 @@ Proof.
   - destruct (Γs !! i) eqn:?; simplify_eq/=.
     rewrite (env_lookup_perm Γs) //=.
     rewrite [(⌜_⌝ ∧ _)%I]and_elim_r.
-    rewrite (comm _ P) -and_sep_assoc.
+    rewrite (comm _ P) -persistent_and_sep_assoc.
     apply and_mono; first done. rewrite comm //.
 Qed.
 
@@ -599,7 +599,7 @@ Proof.
   - apply and_intro; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
       intros j; destruct (ident_beq_reflect j i); naive_solver.
-    + rewrite (comm _ P) -and_sep_assoc.
+    + rewrite (comm _ P) -persistent_and_sep_assoc.
       apply and_mono; first done. rewrite comm //.
 Qed.
 
@@ -734,9 +734,9 @@ Lemma envs_clear_spatial_sound Δ :
   of_envs Δ ⊢ of_envs (envs_clear_spatial Δ) ∗ [∗] env_spatial Δ.
 Proof.
   rewrite !of_envs_eq /envs_clear_spatial /=. apply pure_elim_l=> Hwf.
-  rewrite -and_sep_assoc. apply and_intro.
+  rewrite -persistent_and_sep_assoc. apply and_intro.
   - apply pure_intro. destruct Hwf; constructor; simpl; auto using Enil_wf.
-  - rewrite -and_sep_assoc left_id. done.
+  - rewrite -persistent_and_sep_assoc left_id. done.
 Qed.
 
 Lemma envs_clear_intuitionistic_sound Δ :
@@ -744,7 +744,7 @@ Lemma envs_clear_intuitionistic_sound Δ :
   env_and_persistently (env_intuitionistic Δ) ∗ of_envs (envs_clear_intuitionistic Δ).
 Proof.
   rewrite !of_envs_eq /envs_clear_spatial /=. apply pure_elim_l=> Hwf.
-  rewrite and_sep_1.
+  rewrite persistent_and_sep_1.
   rewrite (pure_True); first by rewrite 2!left_id.
   destruct Hwf. constructor; simpl; auto using Enil_wf.
 Qed.
diff --git a/tests/bi.ref b/tests/bi.ref
index e8fadfb33daa6873da5a4f3f91a562a146713e1e..27b5cb7da314682827854e7c3ab45e03ea45a9bb 100644
--- a/tests/bi.ref
+++ b/tests/bi.ref
@@ -20,72 +20,3 @@ P : PROP
 
 ?p : "Persistent (â–  P)"
 
-The command has indeed failed with message:
-Cannot infer this placeholder of type
-"Separable
-   (True
-    ∧ True
-      ∧ True
-        ∧ True
-          ∧ True
-            ∧ True
-              ∧ True
-                ∧ True
-                  ∧ True
-                    ∧ True
-                      ∧ True
-                        ∧ True
-                          ∧ True
-                            ∧ True
-                              ∧ True
-                                ∧ True
-                                  ∧ True
-                                    ∧ True
-                                      ∧ True
-                                        ∧ True
-                                          ∧ True
-                                            ∧ True
-                                              ∧ True
-                                                ∧ 
-                                                True
-                                                ∧ 
-                                                True
-                                                ∧ 
-                                                True
-                                                ∧ 
-                                                True
-                                                ∧ 
-                                                True
-                                                ∧ 
-                                                True
-                                                ∧ 
-                                                True
-                                                ∧ 
-                                                True
-                                                ∧ 
-                                                True
-                                                ∧ 
-                                                True
-                                                ∧ 
-                                                True
-                                                ∧ 
-                                                True
-                                                ∧ 
-                                                True
-                                                ∧ 
-                                                True
-                                                ∧ 
-                                                True
-                                                ∧ 
-                                                True
-                                                ∧ 
-                                                True
-                                                ∧ 
-                                                True
-                                                ∧ 
-                                                True ∧ True ∧ True ∧ ...)"
-(no type class instance found) in
-environment:
-PROP : bi
-BiPlainly0 : BiPlainly PROP
-P : PROP
diff --git a/tests/bi.v b/tests/bi.v
index 43d549360662ee29cee5700f671fdf62d9863f10..3e38ccce0141b0fe4696c2d13840e7c2170ea205 100644
--- a/tests/bi.v
+++ b/tests/bi.v
@@ -70,12 +70,3 @@ Proof. intros. eexists _. Fail apply _. Abort.
 Goal ∀ {PROP : bi} (P : PROP),
   ∃ plainly_instance, Persistent (@plainly PROP plainly_instance P).
 Proof. intros. eexists _. Fail apply _. Abort.
-
-(** Without the right [Hint Cut] declarations, this will backtrack on trying to
-establish that each conjunction is [Separable], [Persistent], and [Plain], i.e.,
-taking [100^3] steps. *)
-Lemma separable_big `{!BiPlainly PROP} (P : PROP) :
-  Separable (Nat.iter 100 (λ rec, True ∧ rec)%I P).
-Proof.
-  simpl. Fail apply _.
-Abort.