diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index e7cf6bb4cbb41e4c55a2b8a9c9808f7eafc00d76..7389de3a62168f6089396f3a8fad480e160c4c00 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -38,8 +38,8 @@ Proof. intros P. rewrite /Affine. by apply bi.pure_intro. Qed.
 (* Own and valid derived *)
 Lemma persistently_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
 Proof.
-  intros; apply (anti_symm _); first by apply: persistently_elim_absorbing.
-    by rewrite {1}persistently_ownM_core core_id_core.
+  intros; apply (anti_symm _); first by rewrite persistently_elim.
+  by rewrite {1}persistently_ownM_core core_id_core.
 Qed.
 Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False.
 Proof. by intros; rewrite ownM_valid cmra_valid_elim. Qed.
@@ -49,7 +49,7 @@ Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
 Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_empty. Qed.
 Lemma persistently_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
 Proof.
-  intros; apply (anti_symm _); first by apply: persistently_elim_absorbing.
+  intros; apply (anti_symm _); first by rewrite persistently_elim.
   apply:persistently_cmra_valid_1.
 Qed.
 
@@ -93,7 +93,7 @@ Qed.
 (* Derived lemmas for persistence *)
 Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A → uPred M) :
   NonExpansive Φ → LimitPreserving (λ x, Persistent (Φ x)).
-Proof. intros. apply limit_preserving_equiv; solve_proper. Qed.
+Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
 
 (* Persistence *)
 Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index c8488c385c619b10fa1f37564226be40709f05f6..a051d2cb075b004e08f68a5def4cd23bd542db3d 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -200,6 +200,6 @@ Section proofmode_classes.
     FromAnd (own γ a) (own γ b1) (own γ b2).
   Proof.
     intros ? Hb. rewrite /FromAnd (is_op a) own_op.
-    destruct Hb. by rewrite persistent_and_sep_l. by rewrite persistent_and_sep_r.
+    destruct Hb; by rewrite persistent_and_sep.
   Qed.
 End proofmode_classes.
diff --git a/theories/base_logic/proofmode.v b/theories/base_logic/proofmode.v
index f7144fc2abb8b6eb3c8666c79866cb7216a80c68..f252ffe10e4e2c59fcc03f42aae14410d035d8c1 100644
--- a/theories/base_logic/proofmode.v
+++ b/theories/base_logic/proofmode.v
@@ -79,7 +79,7 @@ Global Instance from_sep_ownM_core_id (a b1 b2 : M) :
   FromAnd (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
 Proof.
   intros ? H. rewrite /FromAnd (is_op a) ownM_op.
-  destruct H. by rewrite persistent_and_sep_l. by rewrite persistent_and_sep_r.
+  destruct H; by rewrite persistent_and_sep.
 Qed.
 
 Global Instance into_and_ownM p (a b1 b2 : M) :
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 7b522bf4131cc964eddd07f85a22e87fc8321204..5a0ca25351f8c0f95496dfe34520c797feb3a45f 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -137,7 +137,7 @@ Section sep_list.
     { apply forall_intro=> k; apply forall_intro=> x.
       apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepL_lookup. }
     revert Φ HΦ. induction l as [|x l IH]=> Φ HΦ; [by auto using big_sepL_nil'|].
-    rewrite big_sepL_cons. rewrite -persistent_and_sep_l; apply and_intro.
+    rewrite big_sepL_cons. rewrite -persistent_and_sep; apply and_intro.
     - by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
     - rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)).
   Qed.
@@ -158,21 +158,13 @@ Section sep_list.
       apply forall_intro=> k. by rewrite (forall_elim (S k)).
   Qed.
 
-  Global Instance big_sepL_nil_persistent `{AffineBI PROP} Φ :
+  Global Instance big_sepL_nil_persistent Φ :
     Persistent ([∗ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.
-  Global Instance big_sepL_persistent1 Φ l :
-    (∀ k x, Persistent (Φ k x)) →
-    l ≠ [] →
-    Persistent ([∗ list] k↦x ∈ l, Φ k x).
-  Proof.
-    intros. rewrite /Persistent (big_opL_commute1 bi_persistently (R:=(≡))) //.
-    apply big_opL_proper=> k y ?. by apply persistent_persistently.
-  Qed.
-  Global Instance big_sepL_persistent `{AffineBI PROP} Φ l :
+  Global Instance big_sepL_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_sepL_persistent_id `{AffineBI PROP} Ps :
+  Global Instance big_sepL_persistent_id Ps :
     TCForall Persistent Ps → Persistent ([∗] Ps).
   Proof. induction 1; simpl; apply _. Qed.
 End sep_list.
@@ -404,7 +396,7 @@ Section gmap.
     { apply forall_intro=> k; apply forall_intro=> x.
       apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepM_lookup. }
     induction m as [|i x m ? IH] using map_ind; auto using big_sepM_empty'.
-    rewrite big_sepM_insert // -persistent_and_sep_l. apply and_intro.
+    rewrite big_sepM_insert // -persistent_and_sep. 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.
@@ -431,15 +423,14 @@ Section gmap.
       by rewrite pure_True // True_impl.
   Qed.
 
-  Global Instance big_sepM_empty_persistent `{AffineBI PROP} Φ :
+  Global Instance big_sepM_empty_persistent Φ :
     Persistent ([∗ map] k↦x ∈ ∅, Φ k x).
   Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
-  Global Instance big_sepM_persistent `{AffineBI PROP} Φ m :
+  Global Instance big_sepM_persistent Φ m :
     (∀ k x, Persistent (Φ k x)) → Persistent ([∗ map] k↦x ∈ m, Φ k x).
   Proof. intros. apply big_sepL_persistent=> _ [??]; apply _. Qed.
 End gmap.
 
-
 (** ** Big ops over finite sets *)
 Section gset.
   Context `{Countable A}.
@@ -562,7 +553,7 @@ Section gset.
     { apply forall_intro=> x.
       apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepS_elem_of. }
     induction X as [|x X ? IH] using collection_ind_L; auto using big_sepS_empty'.
-    rewrite big_sepS_insert // -persistent_and_sep_l. apply and_intro.
+    rewrite big_sepS_insert // -persistent_and_sep. apply and_intro.
     - by rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
     - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
       by rewrite pure_True ?True_impl; last set_solver.
@@ -583,11 +574,10 @@ Section gset.
       apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
       by rewrite pure_True ?True_impl; last set_solver.
   Qed.
-
-  Global Instance big_sepS_empty_persistent `{AffineBI PROP} Φ :
+  Global Instance big_sepS_empty_persistent Φ :
     Persistent ([∗ set] x ∈ ∅, Φ x).
   Proof. rewrite /big_opS elements_empty. apply _. Qed.
-  Global Instance big_sepS_persistent `{AffineBI PROP} Φ X :
+  Global Instance big_sepS_persistent Φ X :
     (∀ x, Persistent (Φ x)) → Persistent ([∗ set] x ∈ X, Φ x).
   Proof. rewrite /big_opS. apply _. Qed.
 End gset.
@@ -658,10 +648,10 @@ Section gmultiset.
     □ ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, □ Φ y).
   Proof. apply (big_opMS_commute _). Qed.
 
-  Global Instance big_sepMS_empty_persistent `{AffineBI PROP} Φ :
+  Global Instance big_sepMS_empty_persistent Φ :
     Persistent ([∗ mset] x ∈ ∅, Φ x).
   Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
-  Global Instance big_sepMS_persistent `{AffineBI PROP} Φ X :
+  Global Instance big_sepMS_persistent Φ X :
     (∀ x, Persistent (Φ x)) → Persistent ([∗ mset] x ∈ X, Φ x).
   Proof. rewrite /big_opMS. apply _. Qed.
 End gmultiset.
diff --git a/theories/bi/derived.v b/theories/bi/derived.v
index 6c4bc388b2a9f5ec56322309880e523063eb7715..c76973060f6434a8fcd3afa5bd0df330d4d65f9b 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived.v
@@ -13,7 +13,7 @@ Arguments bi_wand_iff {_} _%I _%I : simpl never.
 Instance: Params (@bi_wand_iff) 1.
 Infix "∗-∗" := bi_wand_iff (at level 95, no associativity) : bi_scope.
 
-Class Persistent {PROP : bi} (P : PROP) := persistent : □ P ⊣⊢ P.
+Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ □ P.
 Arguments Persistent {_} _%I : simpl never.
 Arguments persistent {_} _%I {_}.
 Hint Mode Persistent + ! : typeclass_instances.
@@ -808,9 +808,13 @@ Proof. destruct H. by rewrite (affine Q) right_id. by rewrite absorbing. Qed.
 Lemma sep_elim_r P Q `{H : 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
+    `{HPQ : TCOr (TCAnd (Affine P) (Affine Q)) (TCAnd (Absorbing P) (Absorbing Q))} :
   P ∗ Q ⊢ P ∧ Q.
-Proof. auto using and_intro, sep_elim_l, sep_elim_r. Qed.
+Proof.
+  destruct HPQ as [[??]|[??]];
+    apply and_intro; apply: sep_elim_l || apply: sep_elim_r.
+Qed.
 
 Lemma affine_bare P `{!Affine P} : ■ P ⊣⊢ P.
 Proof. rewrite /bi_bare. apply (anti_symm _); auto. Qed.
@@ -881,31 +885,28 @@ Proof.
 Qed.
 Lemma persistently_and_emp_elim P : emp ∧ □ P ⊢ P.
 Proof. by rewrite comm persistently_and_sep_elim right_id and_elim_r. Qed.
-Lemma persistently_elim P : □ P ⊢ P ∗ True.
+Lemma persistently_elim_True P : □ P ⊢ P ∗ True.
 Proof.
   rewrite -(right_id True%I _ (â–¡ _)%I) -{1}(left_id emp%I _ True%I).
   by rewrite persistently_and_sep_assoc_1 (comm bi_and) persistently_and_emp_elim.
 Qed.
-Lemma persistently_elim_absorbing P `{!Absorbing P} : □ P ⊢ P.
-Proof. by rewrite persistently_elim sep_elim_l. Qed.
+Lemma persistently_elim P `{!Absorbing P} : □ P ⊢ P.
+Proof. by rewrite persistently_elim_True sep_elim_l. Qed.
 
 Lemma persistently_idemp_1 P : □ □ P ⊢ □ P.
-Proof. by rewrite persistently_elim persistently_absorbing. Qed.
+Proof. by rewrite persistently_elim_True persistently_absorbing. Qed.
 Lemma persistently_idemp P : □ □ P ⊣⊢ □ P.
-Proof.
-  apply (anti_symm _); auto using persistently_idemp_1, persistently_idemp_2.
-Qed.
+Proof. apply (anti_symm _); auto using persistently_idemp_1, persistently_idemp_2. Qed.
 
 Lemma persistently_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
 Proof. intros <-. apply persistently_idemp_2. Qed.
 
 Lemma persistently_pure φ : □ ⌜φ⌝ ⊣⊢ ⌜φ⌝.
 Proof.
-  apply (anti_symm _).
-  - by rewrite persistently_elim sep_elim_l.
-  - apply pure_elim'=> Hφ.
-    trans (∀ x : False, □ True : PROP)%I; [by apply forall_intro|].
-    rewrite persistently_forall_2. auto using persistently_mono, pure_intro.
+  apply (anti_symm _); first by rewrite persistently_elim.
+  apply pure_elim'=> Hφ.
+  trans (∀ x : False, □ True : PROP)%I; [by apply forall_intro|].
+  rewrite persistently_forall_2. auto using persistently_mono, pure_intro.
 Qed.
 Lemma persistently_forall {A} (Ψ : A → PROP) : (□ ∀ a, Ψ a) ⊣⊢ (∀ a, □ Ψ a).
 Proof.
@@ -929,11 +930,9 @@ Qed.
 
 Lemma persistently_internal_eq {A : ofeT} (a b : A) : □ (a ≡ b) ⊣⊢ a ≡ b.
 Proof.
-  apply (anti_symm (⊢)); auto using persistently_elim.
-  - rewrite persistently_elim. apply wand_elim_l'.
-    apply (internal_eq_rewrite' a b (λ b, True -∗ a ≡ b)%I); auto using wand_intro_l.
-  - apply (internal_eq_rewrite' a b (λ b, □ (a ≡ b))%I); auto.
-    rewrite -(internal_eq_refl emp%I a). apply persistently_emp_intro.
+  apply (anti_symm (⊢)); first by rewrite persistently_elim.
+  apply (internal_eq_rewrite' a b (λ b, □ (a ≡ b))%I); auto.
+  rewrite -(internal_eq_refl emp%I a). apply persistently_emp_intro.
 Qed.
 
 Lemma persistently_sep_dup P : □ P ⊣⊢ □ P ∗ □ P.
@@ -1017,30 +1016,26 @@ Section persistently_bare_bi.
   Proof.
     apply (anti_symm (⊢)); auto using persistently_impl_wand_2.
     apply persistently_intro', wand_intro_l.
-    by rewrite -persistently_and_sep_r persistently_elim_absorbing impl_elim_r.
+    by rewrite -persistently_and_sep_r persistently_elim impl_elim_r.
   Qed.
 
   Lemma wand_alt P Q : (P -∗ Q) ⊣⊢ ∃ R, R ∗ □ (P ∗ R → Q).
   Proof.
     apply (anti_symm (⊢)).
     - rewrite -(right_id True%I bi_sep (P -∗ Q)%I) -(exist_intro (P -∗ Q)%I).
-      apply sep_mono_r. rewrite -persistently_pure.
-      apply persistently_intro', impl_intro_l.
+      apply sep_mono_r. rewrite -persistently_pure. 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 -persistently_and_sep_r.
-      by rewrite persistently_elim_absorbing impl_elim_r.
+    - apply exist_elim=> R. apply wand_intro_l. rewrite assoc -persistently_and_sep_r.
+      by rewrite persistently_elim impl_elim_r.
   Qed.
   Lemma impl_alt P Q : (P → Q) ⊣⊢ ∃ R, R ∧ □ (P ∧ R -∗ Q).
   Proof.
     apply (anti_symm (⊢)).
     - rewrite -(right_id True%I bi_and (P → Q)%I) -(exist_intro (P → Q)%I).
-      apply and_mono_r. rewrite -persistently_pure.
-      apply persistently_intro', wand_intro_l.
+      apply and_mono_r. rewrite -persistently_pure. apply persistently_intro', wand_intro_l.
       by rewrite impl_elim_r persistently_pure right_id.
-    - apply exist_elim=> R. apply impl_intro_l.
-      rewrite assoc persistently_and_sep_r.
-      by rewrite persistently_elim_absorbing wand_elim_r.
+    - apply exist_elim=> R. apply impl_intro_l. rewrite assoc persistently_and_sep_r.
+      by rewrite persistently_elim wand_elim_r.
   Qed.
 End persistently_bare_bi.
 
@@ -1178,33 +1173,30 @@ Proof. destruct p; simpl; auto using bare_persistently_idemp. Qed.
 (* Persistence *)
 Global Instance Persistent_proper : Proper ((≡) ==> iff) (@Persistent PROP).
 Proof. solve_proper. Qed.
-Lemma persistent_absorbing P : Persistent P → Absorbing P.
-Proof. rewrite /Persistent=> <-. apply _. Qed.
-Hint Immediate persistent_absorbing : typeclass_instances.
 
 Global Instance pure_persistent φ : Persistent (⌜φ⌝%I : PROP).
 Proof. by rewrite /Persistent persistently_pure. Qed.
-Global Instance emp_persistent `{AffineBI PROP} : Persistent (emp%I : PROP).
-Proof. rewrite -True_emp. apply _. Qed.
+Global Instance emp_persistent : Persistent (emp%I : PROP).
+Proof. rewrite /Persistent. apply persistently_emp_intro. Qed.
 Global Instance persistently_persistent P : Persistent (â–¡ P).
-Proof. apply persistently_idemp. Qed.
+Proof. by rewrite /Persistent persistently_idemp. Qed.
 Global Instance and_persistent P Q :
   Persistent P → Persistent Q → Persistent (P ∧ Q).
-Proof. intros. by rewrite /Persistent persistently_and !persistent. Qed.
+Proof. intros. by rewrite /Persistent persistently_and -!persistent. Qed.
 Global Instance or_persistent P Q :
   Persistent P → Persistent Q → Persistent (P ∨ Q).
-Proof. intros. by rewrite /Persistent persistently_or !persistent. Qed.
+Proof. intros. by rewrite /Persistent persistently_or -!persistent. Qed.
 Global Instance forall_persistent {A} (Ψ : A → PROP) :
   (∀ x, Persistent (Ψ x)) → Persistent (∀ x, Ψ x).
 Proof.
   intros. rewrite /Persistent persistently_forall.
-  apply forall_proper=> x. by rewrite !persistent.
+  apply forall_mono=> x. by rewrite -!persistent.
 Qed.
 Global Instance exist_persistent {A} (Ψ : A → PROP) :
   (∀ x, Persistent (Ψ x)) → Persistent (∃ x, Ψ x).
 Proof.
   intros. rewrite /Persistent persistently_exist.
-  apply exist_proper=> x. by rewrite !persistent.
+  apply exist_mono=> x. by rewrite -!persistent.
 Qed.
 
 Global Instance internal_eq_persistent {A : ofeT} (a b : A) :
@@ -1213,61 +1205,74 @@ Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.
 
 Global Instance pure_impl_persistent φ Q : Persistent Q → Persistent (⌜φ⌝ → Q).
 Proof. rewrite pure_impl_forall. apply _. Qed.
-Global Instance pure_wand_persistent φ Q : Persistent Q → Persistent (⌜φ⌝ -∗ Q).
+Global Instance pure_wand_persistent φ Q :
+  Persistent Q → Absorbing Q → Persistent (⌜φ⌝ -∗ Q).
 Proof. intros. rewrite pure_wand_forall. apply _. Qed.
 
 Global Instance sep_persistent P Q :
   Persistent P → Persistent Q → Persistent (P ∗ Q).
-Proof. intros. by rewrite /Persistent persistently_sep !persistent. Qed.
+Proof. intros. by rewrite /Persistent persistently_sep -!persistent. Qed.
 
 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.
 
 (* Properties of persistent propositions *)
-Lemma persistent_persistently P `{!Persistent P} : □ P ⊣⊢ P.
-Proof. by rewrite persistent. Qed.
+Lemma persistent_persistently_2 P `{!Persistent P} : P ⊢ □ P.
+Proof. done. Qed.
+Lemma persistent_persistently P `{!Persistent P, !Absorbing P} : □ P ⊣⊢ P.
+Proof. apply (anti_symm _); auto using persistent_persistently_2, persistently_elim. Qed.
 
 Lemma persistently_intro P Q `{!Persistent P} : (P ⊢ Q) → P ⊢ □ Q.
-Proof. rewrite -(persistent_persistently P); apply persistently_intro'. Qed.
+Proof. intros HP. by rewrite (persistent P) HP. Qed.
+Lemma persistent_and_bare_sep_l_1 P Q `{!Persistent P} : P ∧ Q ⊢ ■ P ∗ Q.
+Proof.
+  rewrite {1}(persistent_persistently_2 P) persistently_and_bare_sep_l.
+  by rewrite -bare_idemp bare_persistently_elim.
+Qed.
+Lemma persistent_and_bare_sep_r_1 P Q `{!Persistent Q} : P ∧ Q ⊢ P ∗ ■ Q.
+Proof. by rewrite !(comm _ P) persistent_and_bare_sep_l_1. Qed.
 
-Lemma persistent_and_sep_l_1 P Q `{!Persistent P} : P ∧ Q ⊢ P ∗ Q.
-Proof. by rewrite -(persistent_persistently P) persistently_and_sep_l_1. Qed.
-Lemma persistent_and_sep_r_1 P Q `{!Persistent Q} : P ∧ Q ⊢ P ∗ Q.
-Proof. by rewrite -(persistent_persistently Q) persistently_and_sep_r_1. Qed.
-Lemma persistent_sep_and P Q `{!Persistent P, !Persistent Q} : P ∗ Q ⊣⊢ P ∧ Q.
+Lemma persistent_and_bare_sep_l P Q `{!Persistent P, !Absorbing P} :
+  P ∧ Q ⊣⊢ ■ P ∗ Q.
+Proof. by rewrite -(persistent_persistently P) persistently_and_bare_sep_l. Qed.
+Lemma persistent_and_bare_sep_r P Q `{!Persistent Q, !Absorbing Q} :
+  P ∧ Q ⊣⊢ P ∗ ■ Q.
+Proof. by rewrite -(persistent_persistently Q) persistently_and_bare_sep_r. Qed.
+
+Lemma persistent_and_sep_1 P Q `{HPQ : !TCOr (Persistent P) (Persistent Q)} :
+  P ∧ Q ⊢ P ∗ Q.
 Proof.
-  by rewrite -(persistent_persistently P) -(persistent_persistently Q)
-             -and_sep_persistently.
+  destruct HPQ.
+  - by rewrite persistent_and_bare_sep_l_1 bare_elim.
+  - by rewrite persistent_and_bare_sep_r_1 bare_elim.
 Qed.
 
-Lemma persistent_sep_dup P `{!Persistent P} : P ⊣⊢ P ∗ P.
+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. by rewrite -(persistent_persistently Q); apply persistently_entails_l. Qed.
+Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
 Lemma persistent_entails_r P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
-Proof. by rewrite -(persistent_persistently Q); apply persistently_entails_r. Qed.
+Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
 
-Lemma persistent_and_sep_assoc P `{!Persistent P} Q R :
+Lemma persistent_and_sep_assoc P `{!Persistent P, !Absorbing P} Q R :
   P ∧ (Q ∗ R) ⊣⊢ (P ∧ Q) ∗ R.
-Proof. by rewrite -(persistent P) persistently_and_sep_assoc. Qed.
+Proof. by rewrite -(persistent_persistently P) persistently_and_sep_assoc. Qed.
 
 Lemma impl_wand_2 P `{!Persistent P} Q : (P -∗ Q) ⊢ P → Q.
-Proof. apply impl_intro_l. by rewrite persistent_and_sep_l_1 wand_elim_r. Qed.
-
-Lemma persistent_and_bare_sep_l P Q `{!Persistent P} : P ∧ Q ⊣⊢ ■ P ∗ Q.
-Proof. by rewrite -(persistent_persistently P) persistently_and_bare_sep_l. Qed.
-Lemma persistent_and_bare_sep_r P Q `{!Persistent Q} : P ∧ Q ⊣⊢ P ∗ ■ Q.
-Proof. by rewrite -(persistent_persistently Q) persistently_and_bare_sep_r. Qed.
+Proof. apply impl_intro_l. by rewrite persistent_and_sep_1 wand_elim_r. Qed.
 
 Section persistent_bi_absorbing.
   Context `{AffineBI PROP}.
 
-  Lemma persistent_and_sep_l  P Q `{!Persistent P} : P ∧ Q ⊣⊢ P ∗ Q.
-  Proof. by rewrite -(persistent_persistently P) persistently_and_sep_l. Qed.
-  Lemma persistent_and_sep_r P Q `{!Persistent Q} : P ∧ Q ⊣⊢ P ∗ Q.
-  Proof. by rewrite -(persistent_persistently Q) persistently_and_sep_r. Qed.
+  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.
@@ -1331,8 +1336,6 @@ Proof.
 Qed.
 End bi_derived.
 
-Hint Immediate persistent_absorbing : typeclass_instances.
-
 Section sbi_derived.
 Context {PROP : sbi}.
 Implicit Types φ : Prop.
@@ -1418,7 +1421,7 @@ Lemma bare_persistently_if_later p P : ⬕?p ▷ P ⊢ ▷ ⬕?p P.
 Proof. destruct p; simpl; auto using bare_persistently_later. Qed.
 
 Global Instance later_persistent P : Persistent P → Persistent (▷ P).
-Proof. intros. by rewrite /Persistent -later_persistently persistent. Qed.
+Proof. intros. by rewrite /Persistent {1}(persistent_persistently_2 P) later_persistently. Qed.
 Global Instance later_absorbing P : Absorbing P → Absorbing (▷ P).
 Proof. intros ? Q. by rewrite {1}(later_intro Q) -later_sep absorbing. Qed.
 
@@ -1606,10 +1609,8 @@ Proof.
 Qed.
 Global Instance persistently_timeless P : Timeless P → Timeless (□ P).
 Proof.
-  intros; rewrite /Timeless.
-  rewrite /bi_except_0 later_persistently_1.
-  rewrite (timeless P) /bi_except_0 persistently_or {1}persistently_elim.
-  apply or_mono; last done. by rewrite sep_elim_l.
+  intros. rewrite /Timeless /bi_except_0 later_persistently_1.
+  by rewrite (timeless P) /bi_except_0 persistently_or {1}persistently_elim.
 Qed.
 
 Global Instance eq_timeless {A : ofeT} (a b : A) :
diff --git a/theories/bi/fractional.v b/theories/bi/fractional.v
index 4f21613ceaf974255140201ca15cf1302d876df3..615d996ab37d1ba75ec6f8228de789412928d98c 100644
--- a/theories/bi/fractional.v
+++ b/theories/bi/fractional.v
@@ -51,8 +51,8 @@ Section fractional.
 
   (** Fractional and logical connectives *)
   Global Instance persistent_fractional P :
-    Persistent P → Fractional (λ _, P).
-  Proof. intros HP q q'. by apply bi.persistent_sep_dup. Qed.
+    Persistent P → Absorbing P → Fractional (λ _, P).
+  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/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 25413547ec0c0ec84348f32cdb637577855a2c66..d1bcf824dd1388ffd5e36fb52636d028dfccfb3b 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -13,7 +13,7 @@ Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
 Proof. by rewrite /IntoInternalEq. Qed.
 Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P :
   IntoInternalEq P x y → IntoInternalEq (□ P) x y.
-Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim_absorbing. Qed.
+Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
 Global Instance into_internal_eq_bare {A : ofeT} (x y : A) P :
   IntoInternalEq P x y → IntoInternalEq (■ P) x y.
 Proof. rewrite /IntoInternalEq=> ->. by rewrite bare_elim. Qed.
@@ -87,7 +87,7 @@ Proof. rewrite /FromPure /IntoPure=> <- ->. by rewrite pure_impl impl_wand_2. Qe
 Global Instance into_pure_bare P φ : IntoPure P φ → IntoPure (■ P) φ.
 Proof. rewrite /IntoPure=> ->. apply bare_elim. Qed.
 Global Instance into_pure_persistently P φ : IntoPure P φ → IntoPure (□ P) φ.
-Proof. rewrite /IntoPure=> ->. apply: persistently_elim_absorbing. Qed.
+Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
 
 (* FromPure *)
 Global Instance from_pure_pure φ : @FromPure PROP ⌜φ⌝ φ.
@@ -115,7 +115,7 @@ Proof. rewrite /FromPure=>Hx. rewrite pure_forall. by setoid_rewrite Hx. Qed.
 
 Global Instance from_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
   FromPure P1 φ1 → FromPure P2 φ2 → FromPure (P1 ∗ P2) (φ1 ∧ φ2).
-Proof. rewrite /FromPure=> <- <-. by rewrite pure_and persistent_and_sep_l_1. Qed.
+Proof. rewrite /FromPure=> <- <-. by rewrite pure_and persistent_and_sep_1. Qed.
 Global Instance from_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
   IntoPure P1 φ1 → FromPure P2 φ2 → FromPure (P1 -∗ P2) (φ1 → φ2).
 Proof.
@@ -140,7 +140,7 @@ Global Instance into_persistent_persistently P : IntoPersistent true P P | 1.
 Proof. by rewrite /IntoPersistent. Qed.
 Global Instance into_persistent_persistent P :
   Persistent P → IntoPersistent false P P | 100.
-Proof. intros. by rewrite /IntoPersistent /= persistent_persistently. Qed.
+Proof. intros. by rewrite /IntoPersistent. Qed.
 
 (* FromPersistent *)
 Global Instance from_persistent_persistently P : FromPersistent (â–¡ P) P | 1.
@@ -169,7 +169,7 @@ Global Instance into_wand_impl_false_true P Q P' :
 Proof.
   rewrite /IntoWand /FromAssumption /= => ? HP. apply wand_intro_l.
   rewrite -(bare_persistently_idemp P) HP.
-  by rewrite -persistently_and_bare_sep_l persistently_elim_absorbing impl_elim_r.
+  by rewrite -persistently_and_bare_sep_l persistently_elim impl_elim_r.
 Qed.
 
 Global Instance into_wand_impl_true_false P Q P' :
@@ -205,7 +205,7 @@ Global Instance into_wand_persistently_true q R P Q :
 Proof. by rewrite /IntoWand /= persistently_idemp. Qed.
 Global Instance into_wand_persistently_false `{!AffineBI PROP} q R P Q :
   IntoWand false q R P Q → IntoWand false q (□ R) P Q.
-Proof. by rewrite /IntoWand persistently_elim_absorbing. Qed.
+Proof. by rewrite /IntoWand persistently_elim. Qed.
 
 Global Instance into_wand_bare_persistently p q R P Q :
   IntoWand p q R P Q → IntoWand p q (⬕ R) P Q.
@@ -217,17 +217,17 @@ Proof. by rewrite /FromAnd. Qed.
 Global Instance from_and_sep_persistent_l P1 P1' P2 :
   FromBare P1 P1' → Persistent P1' → FromAnd (P1 ∗ P2) P1' P2 | 9.
 Proof.
-  rewrite /FromBare /FromAnd=> <- ?. by rewrite persistent_and_bare_sep_l.
+  rewrite /FromBare /FromAnd=> <- ?. by rewrite persistent_and_bare_sep_l_1.
 Qed.
 Global Instance from_and_sep_persistent_r P1 P2 P2' :
   FromBare P2 P2' → Persistent P2' → FromAnd (P1 ∗ P2) P1 P2' | 10.
 Proof.
-  rewrite /FromBare /FromAnd=> <- ?. by rewrite persistent_and_bare_sep_r.
+  rewrite /FromBare /FromAnd=> <- ?. by rewrite persistent_and_bare_sep_r_1.
 Qed.
 Global Instance from_and_sep_persistent P1 P2 :
   Persistent P1 → Persistent P2 → FromAnd (P1 ∗ P2) P1 P2 | 11.
 Proof.
-  rewrite /FromBare /FromAnd. intros ??. by rewrite -persistent_sep_and.
+  rewrite /FromBare /FromAnd. intros ??. by rewrite -persistent_and_sep_1.
 Qed.
 
 Global Instance from_and_pure φ ψ : @FromAnd PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
@@ -243,28 +243,21 @@ Global Instance from_and_persistently_sep P Q1 Q2 :
   FromSep P Q1 Q2 → FromAnd (□ P) (□ Q1) (□ Q2) | 11.
 Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
 
-Hint Extern 10 => assumption : typeclass_instances. (* TODO: move *)
-
 Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat → A → PROP) x l :
   Persistent (Φ 0 x) →
   FromAnd ([∗ list] k ↦ y ∈ x :: l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l, Φ (S k) y).
-Proof. intros. by rewrite /FromAnd big_opL_cons persistent_and_sep_l_1. Qed.
+Proof. intros. by rewrite /FromAnd big_opL_cons persistent_and_sep_1. Qed.
 Global Instance from_and_big_sepL_app_persistent {A} (Φ : nat → A → PROP) l1 l2 :
   (∀ k y, Persistent (Φ k y)) →
   FromAnd ([∗ list] k ↦ y ∈ l1 ++ l2, Φ k y)
     ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
-Proof.
-  intros. rewrite /FromAnd big_opL_app.
-  destruct (decide (l1 = [])) as [->|]; simpl.
-  - by rewrite left_id and_elim_r.
-  - by rewrite persistent_and_sep_l_1.
-Qed.
+Proof. intros. by rewrite /FromAnd big_opL_app persistent_and_sep_1. Qed.
 
 (* FromSep *)
 Global Instance from_sep_sep P1 P2 : FromSep (P1 ∗ P2) P1 P2 | 100.
 Proof. by rewrite /FromSep. Qed.
 Global Instance from_sep_and P1 P2 :
-  TCOr (Affine P1) (Absorbing P2) → TCOr (Affine P2) (Absorbing P1) →
+  TCOr (TCAnd (Affine P1) (Affine P2)) (TCAnd (Absorbing P1) (Absorbing P2)) →
   FromSep (P1 ∧ P2) P1 P2 | 101.
 Proof. intros. by rewrite /FromSep sep_and. Qed.
 
@@ -323,18 +316,18 @@ Global Instance into_sep_and_persistent_l P P' Q :
   Persistent P → FromBare P' P → IntoSep false (P ∧ Q) P' Q.
 Proof.
   rewrite /FromBare /IntoSep /=. intros ? <-.
-  by rewrite persistent_and_bare_sep_l.
+  by rewrite persistent_and_bare_sep_l_1.
 Qed.
 Global Instance into_sep_and_persistent_r P Q Q' :
   Persistent Q → FromBare Q' Q → IntoSep false (P ∧ Q) P Q'.
 Proof.
   rewrite /FromBare /IntoSep /=. intros ? <-.
-  by rewrite persistent_and_bare_sep_r.
+  by rewrite persistent_and_bare_sep_r_1.
 Qed.
 
 Global Instance into_sep_pure p φ ψ : @IntoSep PROP p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof.
-  by rewrite /IntoSep pure_and persistent_and_sep_l_1 bare_persistently_if_sep.
+  by rewrite /IntoSep pure_and persistent_and_sep_1 bare_persistently_if_sep.
 Qed.
 
 Global Instance into_sep_bare p P Q1 Q2 :
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 32bddfd1088189dfcf9d842e5d906f8b255c0404..428cda55c65c9b1172f9e818845ac4bac01f0cd8 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -518,7 +518,7 @@ Proof.
     rewrite right_id. apply impl_intro_l. rewrite bare_and_l persistently_and_sep_r_1.
     by rewrite bare_sep bare_persistently_elim bare_elim wand_elim_r.
   - apply impl_intro_l. rewrite envs_app_sound //; simpl.
-    by rewrite persistent_and_sep_l_1 right_id wand_elim_r.
+    by rewrite persistent_and_sep_1 right_id wand_elim_r.
 Qed.
 Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
   IntoPersistent false P P' →
@@ -635,11 +635,11 @@ Proof.
   intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
   rewrite envs_lookup_sound //.
   rewrite -(idemp bi_and (envs_delete _ _ _)).
-  rewrite {2}envs_simple_replace_sound' //; simpl.
-  rewrite {1}HP1 persistent_and_bare_sep_l -(persistent_persistently P1) assoc.
+  rewrite {2}envs_simple_replace_sound' //; rewrite /= right_id.
+  rewrite {1}HP1 (persistent_persistently_2 P1) persistently_and_bare_sep_l assoc.
   rewrite -bare_persistently_if_idemp -bare_persistently_idemp.
   rewrite (bare_persistently_bare_persistently_if q) -bare_persistently_if_sep.
-  by rewrite into_wand wand_elim_l right_id wand_elim_r.
+  by rewrite into_wand wand_elim_l wand_elim_r.
 Qed.
 
 Lemma tac_specialize_persistent_helper Δ Δ'' j q P R R' Q :
@@ -709,7 +709,8 @@ Lemma tac_assert_persistent Δ Δ1 Δ2 Δ' lr js j P P' Q :
   (Δ1 ⊢ P) → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ???? HP <-. rewrite -(idemp bi_and Δ) {1}envs_split_sound //.
-  rewrite HP sep_elim_l persistent_and_bare_sep_l from_bare.
+  rewrite HP. rewrite (persistent_persistently_2 P) sep_elim_l.
+  rewrite persistently_and_bare_sep_l -bare_idemp bare_persistently_elim from_bare.
   rewrite envs_app_sound //; simpl.
   by rewrite right_id wand_elim_r.
 Qed.