diff --git a/iris/base_logic/lib/own.v b/iris/base_logic/lib/own.v
index 2be0458d2b628c0a3d47e2d5523c6099eec15e98..593835c211201f7650ecf3cc1fcaf6dd779aded8 100644
--- a/iris/base_logic/lib/own.v
+++ b/iris/base_logic/lib/own.v
@@ -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 -persistent_and_sep.
+    rewrite -(exist_intro a'). rewrite -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 persistent_and_sep.
+    destruct Hb; by rewrite and_sep.
   Qed.
 End proofmode_instances.
diff --git a/iris/base_logic/proofmode.v b/iris/base_logic/proofmode.v
index 01cfda35479376f2726f5df5b16b351fb188c53a..30f3dd3e57333e225cf7baf2daf97866d0df1164 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.persistent_and_sep.
+    destruct H; by rewrite bi.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 ad7d004d3ec9cf1b55615172ecd891f790128724..3725368d8641dc386c102f38e6462ed9c0c45200 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 -persistent_and_sep_1 -affinely_and -pure_and.
+    rewrite -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 -persistent_and_sep_1. apply and_intro.
+    rewrite -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 !persistent_and_affinely_sep_l.
+    rewrite !big_sepL2_alt big_sepL_sep !and_affinely_sep_l.
     rewrite -assoc (assoc _ _ (<affine> _)%I). rewrite -(comm bi_sep (<affine> _)%I).
-    rewrite -assoc (assoc _ _ (<affine> _)%I) -!persistent_and_affinely_sep_l.
-    by rewrite affinely_and_r persistent_and_affinely_sep_l idemp.
+    rewrite -assoc (assoc _ _ (<affine> _)%I) -!and_affinely_sep_l.
+    by rewrite affinely_and_r 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 -persistent_and_sep_1. apply and_intro.
+    rewrite -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 -!persistent_and_sep_assoc.
+  rewrite !big_sepL2_alt [(_ ∗ _)%I]comm -!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 !persistent_and_affinely_sep_l !assoc (comm _ P).
+    by rewrite !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 -persistent_and_sep_1 -affinely_and -pure_and map_Forall_insert.
+    by rewrite -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 // -persistent_and_sep_1. apply and_intro.
+    rewrite big_sepM_insert // -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 !persistent_and_affinely_sep_l /=.
+    rewrite !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 !persistent_and_affinely_sep_l /=.
+    rewrite !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 !persistent_and_affinely_sep_l /=.
+    rewrite !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 !persistent_and_affinely_sep_l /=.
+    rewrite !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 -persistent_and_sep_1 -affinely_and -pure_and.
+    rewrite -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 // -persistent_and_sep_1. apply and_intro.
+    rewrite big_sepS_insert // -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 -persistent_and_sep_1 -affinely_and -pure_and.
+    rewrite -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 -persistent_and_sep_1. apply and_intro.
+    rewrite big_sepMS_singleton -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_laws.v b/iris/bi/derived_laws.v
index 835d58db621161821a7e1cf1703cd4a6b3d89a8f..019ba5fab0c397cee81568dcce1dcf9f7f6b0a45 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -1078,14 +1078,12 @@ Proof.
   by rewrite {1}HP persistently_and_sep_elim_emp.
 Qed.
 
-Lemma persistently_and_sep_assoc P Q R : <pers> P ∧ (Q ∗ R) ⊣⊢ (<pers> P ∧ Q) ∗ R.
-Proof. apply: and_sep_assoc. 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 persistently_and_sep_assoc.
+  rewrite and_sep_assoc.
   rewrite (comm bi_and) persistently_and_emp_elim comm //.
 Qed.
 Lemma persistently_elim P `{!Absorbing P} : <pers> P ⊢ P.
@@ -1111,19 +1109,11 @@ Proof.
   auto using persistently_mono, pure_intro.
 Qed.
 
-Lemma persistently_sep_dup P : <pers> P ⊣⊢ <pers> P ∗ <pers> P.
-Proof. apply: sep_dup. Qed.
-
-Lemma persistently_and_sep_l_1 P Q : <pers> P ∧ Q ⊢ <pers> P ∗ Q.
-Proof. apply: and_sep_l_1. Qed.
-Lemma persistently_and_sep_r_1 P Q : P ∧ <pers> Q ⊢ P ∗ <pers> Q.
-Proof. apply: and_sep_r_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 persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim.
+  by rewrite and_sep_assoc (comm bi_and) persistently_and_emp_elim.
 Qed.
 
 Lemma persistently_affinely_elim P : <pers> <affine> P ⊣⊢ <pers> P.
@@ -1167,41 +1157,30 @@ 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.
+Proof. intros; rewrite -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.
+Proof. intros; rewrite -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) persistently_and_sep_assoc.
+  rewrite -{2}(emp_sep P) 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_wand_2. 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: and_sep_l. Qed.
-  Lemma persistently_and_sep_r P Q : P ∧ <pers> Q ⊣⊢ P ∗ <pers> Q.
-  Proof. apply: and_sep_r. 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 -persistently_and_sep_r persistently_elim impl_elim_r.
+    by rewrite -and_sep_r persistently_elim impl_elim_r.
   Qed.
 
-  Lemma impl_wand_persistently P Q : (<pers> P → Q) ⊣⊢ (<pers> P -∗ Q).
-  Proof. apply: impl_wand. Qed.
-
   Lemma wand_alt P Q : (P -∗ Q) ⊣⊢ ∃ R, R ∗ <pers> (P ∗ R → Q).
   Proof.
     apply (anti_symm (⊢)).
@@ -1210,7 +1189,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 -persistently_and_sep_r.
+      rewrite assoc -and_sep_r.
       by rewrite persistently_elim impl_elim_r.
   Qed.
 End persistently_affine_bi.
@@ -1610,54 +1589,16 @@ 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. apply: and_affinely_sep_l_1. Qed.
-Lemma persistent_and_affinely_sep_r_1 P Q `{!Persistent Q} :
-  P ∧ Q ⊢ P ∗ <affine> Q.
-Proof. apply: and_affinely_sep_r_1. Qed.
-
-Lemma persistent_and_sep_1 P Q `{HPQ : !TCOr (Persistent P) (Persistent Q)} :
-  P ∧ Q ⊢ P ∗ Q.
-Proof. apply and_sep_1; destruct HPQ; apply _. Qed.
-
-Lemma persistent_sep_dup P
-    `{HP : !TCOr (Affine P) (Absorbing P), !Persistent P} :
-  P ⊣⊢ P ∗ P.
-Proof. apply: sep_dup. Qed.
 
 Lemma persistent_entails_l P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ Q ∗ P.
-Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
+Proof. intros. rewrite -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.
+Proof. intros. rewrite -and_sep_1; auto. Qed.
 
 Lemma absorbingly_intuitionistically_into_persistently P :
   <absorb> □ P ⊣⊢ <pers> P.
 Proof. apply: absorbingly_affinely. Qed.
 
-Lemma persistent_absorbingly_affinely_2 P `{!Persistent P} :
-  P ⊢ <absorb> <affine> P.
-Proof. apply: absorbingly_affinely_2. Qed.
-
-Lemma persistent_impl_wand_2 P `{!Persistent P} Q : (P -∗ Q) ⊢ P → Q.
-Proof. apply: impl_wand_2. Qed.
-
-Lemma persistent_and_affinely_sep_l P Q `{!Persistent P, !Absorbing P} :
-  P ∧ Q ⊣⊢ <affine> P ∗ Q.
-Proof. apply: and_affinely_sep_l. Qed.
-Lemma persistent_and_affinely_sep_r P Q `{!Persistent Q, !Absorbing Q} :
-  P ∧ Q ⊣⊢ P ∗ <affine> Q.
-Proof. apply: and_affinely_sep_r. Qed.
-Lemma persistent_and_sep_assoc P `{!Persistent P, !Absorbing P} Q R :
-  P ∧ (Q ∗ R) ⊣⊢ (P ∧ Q) ∗ R.
-Proof. apply: and_sep_assoc. Qed.
-Lemma persistent_absorbingly_affinely P `{!Persistent P, !Absorbing P} :
-  <absorb> <affine> P ⊣⊢ P.
-Proof. apply: absorbingly_affinely. Qed.
-Lemma persistent_impl_wand_affinely P `{!Persistent P, !Absorbing P} Q :
-  (P → Q) ⊣⊢ (<affine> P -∗ Q).
-Proof. apply: impl_wand_affinely. Qed.
-
 (** We don't have a [Intuitionistic] typeclass, but if we did, this
 would be its only field. *)
 Lemma intuitionistic P `{!Persistent P, !Affine P} : P ⊢ □ P.
@@ -1666,21 +1607,6 @@ 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 persistent_impl_wand P `{!Persistent P} Q : (P → Q) ⊣⊢ (P -∗ Q).
-  Proof. apply: impl_wand. Qed.
-End persistent_bi_absorbing.
-
 (* 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 d89ef824376e443981197beb48803f79876a9b36..fff6581fd6f1447ccd86ac9246af6ed734f6e6dc 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 -persistently_sep_dup.
+    by rewrite -!or_intro_l -persistently_pure -later_sep -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) persistent_and_sep_assoc impl_elim_r wand_elim_l.
+  by rewrite (comm _ P) 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/lib/fractional.v b/iris/bi/lib/fractional.v
index 6b985d9ecc7902dd0c40f50544bf7e190472a81b..b8d3de822c60c5834fbfe5fd5f4feb50b3343526 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.persistent_sep_dup. Qed.
+  Proof. intros ?? q q'. apply: bi.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 7607746589761a76889b59bd213fe4b3ea6e1ba1..f91d9ffdead1749ac104d88953d374a5748dcaf5 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -161,7 +161,7 @@ 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.
+  Proof. by rewrite -(persistently_elim_plainly P) 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.
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index ade5e63773b5ee6a51c0bddf63da442b8038a937..fa991df734628eb2e954763113907f9c3b43e85a 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 !persistent_and_affinely_sep_l.
+    rewrite !big_sepL2_alt !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 765cd82abfa9c080cb0536ac705e92e16feeaeed..44124d6cbaffae7c0a5ca7a9c02aa83cb5ba45bf 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 -persistent_and_affinely_sep_l affinely_if_and_r.
-  - by rewrite pure_and -affinely_affinely_if -persistent_and_affinely_sep_r_1.
+  - by rewrite pure_and -and_affinely_sep_l affinely_if_and_r.
+  - by rewrite pure_and -affinely_affinely_if -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 -persistent_and_affinely_sep_r -(affine_affinely P1) HP1.
+    rewrite -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 -persistent_absorbingly_affinely_2.
+  by rewrite -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 persistent_impl_wand_affinely wand_elim_r //.
+  - rewrite 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 persistent_impl_wand_affinely.
+  rewrite 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 -persistent_impl_wand_affinely.
+  by rewrite -pure_impl_forall -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 persistent_and_affinely_sep_l_1 {1}(persistent_persistently_2 P1).
+  rewrite 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 persistent_and_affinely_sep_r_1 {1}(persistent_persistently_2 P2).
+  rewrite 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 persistent_and_sep_1. Qed.
+Proof. rewrite /IsCons=> -> ?. by rewrite /FromAnd big_sepL_cons 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 persistent_and_sep_1. Qed.
+Proof. rewrite /IsApp=> -> ?. by rewrite /FromAnd big_sepL_app 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 persistent_and_sep_1.
+  by rewrite /FromAnd big_sepL2_cons 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 persistent_and_sep_1.
+  rewrite /IsApp=> -> -> ?. rewrite /FromAnd 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 persistent_and_sep_1. Qed.
+Proof. intros. by rewrite /FromAnd big_sepMS_disj_union 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 persistent_and_affinely_sep_l_1.
-  - by rewrite persistent_and_affinely_sep_l_1.
+    by rewrite and_affinely_sep_l_1.
+  - by rewrite 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 persistent_and_affinely_sep_r_1.
-  - by rewrite persistent_and_affinely_sep_r_1.
+    by rewrite and_affinely_sep_r_1.
+  - by rewrite and_affinely_sep_r_1.
 Qed.
 
 Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
-Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.
+Proof. by rewrite /IntoSep pure_and 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 persistently_and_sep_l_1.
+  by rewrite sep_and persistently_and 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) -persistent_and_affinely_sep_r.
+  - rewrite -(affine_affinely P) (into_pure P) -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 e3c78d51eb4e9a5c49f7c7cfc3e908d52a2d014a..583e883862915478a09c346e638c295e50ffb6ef 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 -persistently_and_sep_l_1
+  by rewrite -persistently_sep_2 -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 6ee58f912c64b1c26450a6cb11e61ef0502ccbdc..0d14c49f81806a47c15f3d500119c0b403595a78 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) persistent_and_sep_1.
+  rewrite -(idemp bi_and (<affine> â–· False)%I) 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 0971f80cd2681716ba5cd883c0631061efb0010f..21e2b31500a787e27395455173e0cd090acb7f68 100644
--- a/iris/proofmode/class_instances_plainly.v
+++ b/iris/proofmode/class_instances_plainly.v
@@ -60,7 +60,8 @@ 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 plainly_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 06b7f5690b237b6d4646c9b8709273676a83ea01..8c4495fdcb557527b6d0a98ef04914dd050e69aa 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 -persistent_and_sep_assoc left_id //.
+    rewrite /bi_affinely [(emp ∧ _)%I]comm -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) -persistent_and_affinely_sep_l.
+    + rewrite -(affine_affinely P) (into_pure P) -and_affinely_sep_l.
       by apply pure_elim_l.
-    + rewrite (into_pure P) -(persistent_absorbingly_affinely ⌜ _ ⌝) absorbingly_sep_lr.
-      rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
+    + rewrite (into_pure P) -(absorbingly_affinely ⌜ _ ⌝) absorbingly_sep_lr.
+      rewrite -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) persistent_and_affinely_sep_l_1 wand_elim_r.
+    by rewrite -(from_affinely P' P) 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 persistent_and_affinely_sep_r -assoc. apply wand_elim_r'.
-  rewrite -persistent_and_affinely_sep_r. apply impl_elim_r'. destruct d.
+  rewrite and_affinely_sep_r -assoc. apply wand_elim_r'.
+  rewrite -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 !persistent_and_affinely_sep_l.
+    rewrite !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]persistent_and_affinely_sep_l.
+  rewrite ![(env_and_persistently _ ∧ _)%I]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 46a92dbdc1785fafe7e7e1ce1941ad9855ffb930..5ca457c899806208c0aa227dffdb97bb2c3b082f 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 -persistent_and_affinely_sep_l. f_equiv.
+  rewrite -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 persistent_and_sep_assoc. done.
+    rewrite 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) -persistent_and_sep_assoc.
+    rewrite (comm _ P) -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) -persistent_and_sep_assoc.
+    + rewrite (comm _ P) -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 -persistent_and_sep_assoc. apply and_intro.
+  rewrite -and_sep_assoc. apply and_intro.
   - apply pure_intro. destruct Hwf; constructor; simpl; auto using Enil_wf.
-  - rewrite -persistent_and_sep_assoc left_id. done.
+  - rewrite -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 persistent_and_sep_1.
+  rewrite and_sep_1.
   rewrite (pure_True); first by rewrite 2!left_id.
   destruct Hwf. constructor; simpl; auto using Enil_wf.
 Qed.