diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index a051d2cb075b004e08f68a5def4cd23bd542db3d..308331a0466e19fe6bd6a0b42f21526eb4afd6d3 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -185,8 +185,8 @@ Section proofmode_classes.
   Context `{inG Σ A}.
   Implicit Types a b : A.
 
-  Global Instance into_sep_own p γ a b1 b2 :
-    IsOp a b1 b2 → IntoSep p (own γ a) (own γ b1) (own γ b2).
+  Global Instance into_sep_own γ a b1 b2 :
+    IsOp a b1 b2 → IntoSep (own γ a) (own γ b1) (own γ b2).
   Proof. intros. by rewrite /IntoSep (is_op a) own_op. Qed.
   Global Instance into_and_own p γ a b1 b2 :
     IsOp a b1 b2 → IntoAnd p (own γ a) (own γ b1) (own γ b2).
diff --git a/theories/base_logic/proofmode.v b/theories/base_logic/proofmode.v
index f252ffe10e4e2c59fcc03f42aae14410d035d8c1..ac7c11bef72ddaa2271754f5438f9923f1a43f40 100644
--- a/theories/base_logic/proofmode.v
+++ b/theories/base_logic/proofmode.v
@@ -88,8 +88,8 @@ Proof.
   intros. apply bare_persistently_if_mono. by rewrite (is_op a) ownM_op sep_and.
 Qed.
 
-Global Instance into_sep_ownM p (a b1 b2 : M) :
-  IsOp a b1 b2 → IntoSep p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Global Instance into_sep_ownM (a b1 b2 : M) :
+  IsOp a b1 b2 → IntoSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
 Proof. intros. by rewrite /IntoSep (is_op a) ownM_op. Qed.
 
 Global Instance from_sep_bupd P Q1 Q2 :
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index eaa3fe780904da2b5b3ed48937430075ee5a7736..29695fe3578296c4ba79b2afd57b2c057cd3c10d 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -438,9 +438,6 @@ Proof.
   - (* (P ⊢ Q -∗ R) → P ∗ Q ⊢ R *)
     intros P Q R. unseal=> HPQR. split; intros n x ? (?&?&?&?&?). ofe_subst.
     eapply HPQR; eauto using cmra_validN_op_l.
-  - (* emp ∧ (Q ∗ R) ⊢ (emp ∧ Q) ∗ R (ADMISSIBLE) *)
-    intros Q R. unfold uPred_emp; unseal; split; intros n x ? [_ (x1&x2&?&?&?)].
-    exists x1, x2; simpl; auto. 
   - (* (P ⊢ Q) → □ P ⊢ □ Q *)
     intros P QR HP. unseal; split=> n x ? /=. by apply HP, cmra_core_validN.
   - (* □ P ⊢ □ □ P *)
diff --git a/theories/bi/derived.v b/theories/bi/derived.v
index c76973060f6434a8fcd3afa5bd0df330d4d65f9b..d08f72e307662d837a8956342b8b8625469a1dc0 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived.v
@@ -34,6 +34,9 @@ Hint Mode Affine + ! : typeclass_instances.
 Class AffineBI (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
 Existing Instance absorbing_bi | 0.
 
+Class PositiveBI (PROP : bi) :=
+  positive_bi (P Q : PROP) : ■ (P ∗ Q) ⊢ ■ P ∗ Q.
+
 Class Absorbing {PROP : bi} (P : PROP) := absorbing Q : P ∗ Q ⊢ P.
 Arguments Absorbing {_} _%I : simpl never.
 Arguments absorbing {_} _%I _%I.
@@ -705,28 +708,22 @@ Proof.
   rewrite /bi_bare -(comm _ P) (assoc _ (_ ∧ _)%I) -!(assoc _ P).
   by rewrite idemp !assoc (comm _ P).
 Qed.
-Lemma bare_sep P Q : ■ (P ∗ Q) ⊣⊢ ■ P ∗ ■ Q.
+Lemma bare_sep_2 P Q : ■ P ∗ ■ Q ⊢ ■ (P ∗ Q).
 Proof.
-  rewrite /bi_bare. apply (anti_symm _).
-  - rewrite -{1}(idemp bi_and emp%I) -assoc emp_and_sep_assoc_1.
-    by rewrite (comm bi_sep) emp_and_sep_assoc_1 comm.
-  - apply and_intro.
-    + by rewrite !and_elim_l right_id.
-    + by rewrite !and_elim_r.
+  rewrite /bi_bare. apply and_intro.
+  - by rewrite !and_elim_l right_id.
+  - by rewrite !and_elim_r.
+Qed.
+Lemma bare_sep `{PositiveBI PROP} P Q : ■ (P ∗ Q) ⊣⊢ ■ P ∗ ■ Q.
+Proof.
+  apply (anti_symm _), bare_sep_2.
+  by rewrite -{1}bare_idemp positive_bi !(comm _ (â–  P)%I) positive_bi.
 Qed.
 Lemma bare_forall {A} (Φ : A → PROP) : ■ (∀ a, Φ a) ⊢ ∀ a, ■ Φ a.
 Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
 Lemma bare_exist {A} (Φ : A → PROP) : ■ (∃ a, Φ a) ⊣⊢ ∃ a, ■ Φ a.
 Proof. by rewrite /bi_bare and_exist_l. Qed.
 
-Lemma bare_sep_l P Q : ■ (P ∗ Q) ⊢ ■ P.
-Proof.
-  rewrite /bi_bare. apply and_intro; auto.
-  by rewrite (comm _ P) emp_and_sep_assoc_1 {1}and_elim_l left_id.
-Qed.
-Lemma bare_sep_r P Q : ■ (P ∗ Q) ⊢ ■ Q.
-Proof. by rewrite (comm _ P) bare_sep_l. Qed.
-
 Lemma bare_True_emp : ■ True ⊣⊢ ■ emp.
 Proof. apply (anti_symm _); rewrite /bi_bare; auto. Qed.
 
@@ -838,8 +835,10 @@ Proof. apply (anti_symm _); auto using sep_True_2. Qed.
 Section affine_bi.
   Context `{AffineBI PROP}.
 
-  Global Instance affine_bi P : Absorbing P | 0.
+  Global Instance affine_bi_absorbing P : Absorbing P | 0.
   Proof. intros Q. by rewrite (affine Q) right_id. Qed.
+  Global Instance affine_bi_positive : PositiveBI PROP.
+  Proof. intros P Q. by rewrite !affine_bare. Qed.
 
   Lemma True_emp : True ⊣⊢ emp.
   Proof. apply (anti_symm _); auto using affine. Qed.
@@ -876,19 +875,23 @@ Proof. intros P Q; apply persistently_mono. Qed.
 Global Instance persistently_absorbing P : Absorbing (â–¡ P).
 Proof. rewrite /Absorbing=> R. apply persistently_absorbing. Qed.
 
-Lemma persistently_and_sep_assoc_1 P Q R : □ P ∧ (Q ∗ R) ⊢ (□ P ∧ Q) ∗ R.
+Lemma persistently_and_sep_assoc P Q R : □ P ∧ (Q ∗ R) ⊣⊢ (□ P ∧ Q) ∗ R.
 Proof.
-  rewrite {1}persistently_idemp_2 persistently_and_sep_elim assoc.
-  apply sep_mono_l, and_intro.
-  - by rewrite and_elim_r absorbing.
-  - by rewrite and_elim_l left_id.
+  apply (anti_symm (⊢)).
+  - rewrite {1}persistently_idemp_2 persistently_and_sep_elim assoc.
+    apply sep_mono_l, and_intro.
+    + by rewrite and_elim_r absorbing.
+    + 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 ∧ □ P ⊢ P.
 Proof. by rewrite comm persistently_and_sep_elim right_id and_elim_r. Qed.
 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.
+  by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim.
 Qed.
 Lemma persistently_elim P `{!Absorbing P} : □ P ⊢ P.
 Proof. by rewrite persistently_elim_True sep_elim_l. Qed.
@@ -939,24 +942,9 @@ Lemma persistently_sep_dup P : □ P ⊣⊢ □ P ∗ □ P.
 Proof.
   apply (anti_symm _); last by eauto using sep_elim_l with typeclass_instances.
   rewrite -{1}(idemp bi_and (â–¡ _)%I) -{2}(left_id emp%I _ (â–¡ _)%I).
-  by rewrite persistently_and_sep_assoc_1 and_elim_l.
+  by rewrite persistently_and_sep_assoc and_elim_l.
 Qed.
 
-Lemma persistently_and_sep_assoc P Q R : □ P ∧ (Q ∗ R) ⊣⊢ (□ P ∧ Q) ∗ R.
-Proof.
-  apply (anti_symm (⊢)); auto using persistently_and_sep_assoc_1.
-  apply and_intro.
-  - by rewrite and_elim_l sep_elim_l.
-  - by rewrite and_elim_r.
-Qed.
-Lemma persistently_sep_elim_l P Q : □ (P ∗ Q) ⊢ □ P.
-Proof.
-  rewrite -(left_id True%I bi_and (â–¡ _)%I) (persistently_emp_intro True%I).
-  by rewrite -persistently_and (comm bi_sep) emp_and_sep_assoc_1 and_elim_l left_id.
-Qed.
-Lemma persistently_sep_elim_r P Q : □ (P ∗ Q) ⊢ □ Q.
-Proof. by rewrite comm persistently_sep_elim_l. Qed.
-
 Lemma persistently_and_sep_l_1 P Q : □ P ∧ Q ⊢ □ P ∗ Q.
 Proof.
   by rewrite -{1}(left_id emp%I _ Q%I) persistently_and_sep_assoc and_elim_l.
@@ -966,12 +954,17 @@ Proof. by rewrite !(comm _ P) persistently_and_sep_l_1. Qed.
 
 Lemma persistently_True_emp : □ True ⊣⊢ □ emp.
 Proof. apply (anti_symm _); auto using persistently_emp_intro. Qed.
-Lemma persistently_and_sep P Q : □ (P ∧ Q) ⊣⊢ □ (P ∗ Q).
+Lemma persistently_and_sep P Q : □ (P ∧ Q) ⊢ □ (P ∗ Q).
 Proof.
-  rewrite persistently_and. apply (anti_symm (⊢)).
-  - rewrite -{1}persistently_idemp -persistently_and -{1}(left_id emp%I _ Q%I).
-    by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim.
-  - auto using persistently_sep_elim_l, persistently_sep_elim_r.
+  rewrite persistently_and.
+  rewrite -{1}persistently_idemp -persistently_and -{1}(left_id emp%I _ Q%I).
+  by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim.
+Qed.
+
+Lemma persistently_bare P : □ ■ P ⊣⊢ □ P.
+Proof.
+  by rewrite /bi_bare persistently_and -persistently_True_emp
+             persistently_pure left_id.
 Qed.
 
 Lemma and_sep_persistently P Q : □ P ∧ □ Q ⊣⊢ □ P ∗ □ Q.
@@ -980,11 +973,17 @@ Proof.
   - auto using persistently_and_sep_l_1.
   - eauto 10 using sep_elim_l, sep_elim_r with typeclass_instances.
 Qed.
-Lemma persistently_sep P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
+Lemma persistently_sep_2 P Q : □ P ∗ □ Q ⊢ □ (P ∗ Q).
 Proof. by rewrite -persistently_and_sep persistently_and -and_sep_persistently. Qed.
+Lemma persistently_sep `{PositiveBI PROP} P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
+Proof.
+  apply (anti_symm _); auto using persistently_sep_2.
+  by rewrite -persistently_bare bare_sep sep_and !bare_elim persistently_and
+             and_sep_persistently.
+Qed.
 
 Lemma persistently_wand P Q : □ (P -∗ Q) ⊢ □ P -∗ □ Q.
-Proof. by apply wand_intro_r; rewrite -persistently_sep wand_elim_l. Qed.
+Proof. apply wand_intro_r. by rewrite persistently_sep_2 wand_elim_l. Qed.
 
 Lemma persistently_entails_l P Q : (P ⊢ □ Q) → P ⊢ □ Q ∗ P.
 Proof. intros; rewrite -persistently_and_sep_l_1; auto. Qed.
@@ -1023,53 +1022,48 @@ Section persistently_bare_bi.
   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.
+    - 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 wand_elim_r.
   Qed.
 End persistently_bare_bi.
 
-(* The combined bare persistently modality *)
-Lemma persistently_bare P : □ ■ P ⊣⊢ □ P.
-Proof.
-  by rewrite /bi_bare persistently_and -persistently_True_emp
-             persistently_pure left_id.
-Qed.
 
+(* The combined bare persistently modality *)
 Lemma bare_persistently_elim P : ⬕ P ⊢ P.
 Proof. apply persistently_and_emp_elim. Qed.
 Lemma bare_persistently_intro' P Q : (⬕ P ⊢ Q) → ⬕ P ⊢ ⬕ Q.
 Proof. intros <-. by rewrite persistently_bare persistently_idemp. Qed.
 
 Lemma bare_persistently_emp : ⬕ emp ⊣⊢ emp.
-Proof.
-  by rewrite -persistently_True_emp persistently_pure bare_True_emp bare_emp.
-Qed.
+Proof. by rewrite -persistently_True_emp persistently_pure bare_True_emp bare_emp. Qed.
 Lemma bare_persistently_and P Q : ⬕ (P ∧ Q) ⊣⊢ ⬕ P ∧ ⬕ Q.
 Proof. by rewrite persistently_and bare_and. Qed.
 Lemma bare_persistently_or P Q : ⬕ (P ∨ Q) ⊣⊢ ⬕ P ∨ ⬕ Q.
 Proof. by rewrite persistently_or bare_or. Qed.
 Lemma bare_persistently_exist {A} (Φ : A → PROP) : ⬕ (∃ x, Φ x) ⊣⊢ ∃ x, ⬕ Φ x.
 Proof. by rewrite persistently_exist bare_exist. Qed.
-Lemma bare_persistently_sep P Q : ⬕ (P ∗ Q) ⊣⊢ ⬕ P ∗ ⬕ Q.
-Proof. by rewrite persistently_sep bare_sep. Qed.
+Lemma bare_persistently_sep_2 P Q : ⬕ P ∗ ⬕ Q ⊢ ⬕ (P ∗ Q).
+Proof. by rewrite bare_sep_2 persistently_sep_2. Qed.
+Lemma bare_persistently_sep `{PositiveBI PROP} P Q : ⬕ (P ∗ Q) ⊣⊢ ⬕ P ∗ ⬕ Q.
+Proof. by rewrite -bare_sep -persistently_sep. Qed.
 
 Lemma bare_persistently_idemp P : ⬕ ⬕ P ⊣⊢ ⬕ P.
 Proof. by rewrite persistently_bare persistently_idemp. Qed.
 
-Lemma bare_persistently_sep_dup P : ⬕ P ⊣⊢ ⬕ P ∗ ⬕ P.
-Proof. by rewrite {1}persistently_sep_dup bare_sep. Qed.
-
 Lemma persistently_and_bare_sep_l P Q : □ P ∧ Q ⊣⊢ ⬕ P ∗ Q.
 Proof.
   apply (anti_symm _).
@@ -1078,6 +1072,11 @@ Proof.
 Qed.
 Lemma persistently_and_bare_sep_r P Q : P ∧ □ Q ⊣⊢ P ∗ ⬕ Q.
 Proof. by rewrite !(comm _ P) persistently_and_bare_sep_l. Qed.
+Lemma and_sep_bare_persistently P Q : ⬕ P ∧ ⬕ Q ⊣⊢ ⬕ P ∗ ⬕ Q.
+Proof. by rewrite -persistently_and_bare_sep_l -bare_and bare_and_l. Qed.
+
+Lemma bare_persistently_sep_dup P : ⬕ P ⊣⊢ ⬕ P ∗ ⬕ P.
+Proof. by rewrite -persistently_and_bare_sep_l bare_and_l bare_and idemp. Qed.
 
 (* Conditional bare modality *)
 Global Instance bare_if_ne p : NonExpansive (@bi_bare_if PROP p).
@@ -1108,7 +1107,9 @@ Lemma bare_if_or p P Q : ■?p (P ∨ Q) ⊣⊢ ■?p P ∨ ■?p Q.
 Proof. destruct p; simpl; auto using bare_or. Qed.
 Lemma bare_if_exist {A} p (Ψ : A → PROP) : (■?p ∃ a, Ψ a) ⊣⊢ ∃ a, ■?p Ψ a.
 Proof. destruct p; simpl; auto using bare_exist. Qed.
-Lemma bare_if_sep p P Q : ■?p (P ∗ Q) ⊣⊢ ■?p P ∗ ■?p Q.
+Lemma bare_if_sep_2 p P Q : ■?p P ∗ ■?p Q ⊢ ■?p (P ∗ Q).
+Proof. destruct p; simpl; auto using bare_sep_2. Qed.
+Lemma bare_if_sep `{PositiveBI PROP} p P Q : ■?p (P ∗ Q) ⊣⊢ ■?p P ∗ ■?p Q.
 Proof. destruct p; simpl; auto using bare_sep. Qed.
 
 Lemma bare_if_idemp p P : ■?p ■?p P ⊣⊢ ■?p P.
@@ -1138,7 +1139,9 @@ Lemma persistently_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q.
 Proof. destruct p; simpl; auto using persistently_or. Qed.
 Lemma persistently_if_exist {A} p (Ψ : A → PROP) : (□?p ∃ a, Ψ a) ⊣⊢ ∃ a, □?p Ψ a.
 Proof. destruct p; simpl; auto using persistently_exist. Qed.
-Lemma persistently_if_sep p P Q : □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q.
+Lemma persistently_if_sep_2 p P Q : □?p P ∗ □?p Q ⊢ □?p (P ∗ Q).
+Proof. destruct p; simpl; auto using persistently_sep_2. Qed.
+Lemma persistently_if_sep `{PositiveBI PROP} p P Q : □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q.
 Proof. destruct p; simpl; auto using persistently_sep. Qed.
 
 Lemma persistently_if_idemp p P : □?p □?p P ⊣⊢ □?p P.
@@ -1161,10 +1164,11 @@ Lemma bare_persistently_if_and p P Q : ⬕?p (P ∧ Q) ⊣⊢ ⬕?p P ∧ ⬕?p
 Proof. destruct p; simpl; auto using bare_persistently_and. Qed.
 Lemma bare_persistently_if_or p P Q : ⬕?p (P ∨ Q) ⊣⊢ ⬕?p P ∨ ⬕?p Q.
 Proof. destruct p; simpl; auto using bare_persistently_or. Qed.
-Lemma bare_persistently_if_exist {A} p (Ψ : A → PROP) :
-  (⬕?p ∃ a, Ψ a) ⊣⊢ ∃ a, ⬕?p Ψ a.
+Lemma bare_persistently_if_exist {A} p (Ψ : A → PROP) : (⬕?p ∃ a, Ψ a) ⊣⊢ ∃ a, ⬕?p Ψ a.
 Proof. destruct p; simpl; auto using bare_persistently_exist. Qed.
-Lemma bare_persistently_if_sep p P Q : ⬕?p (P ∗ Q) ⊣⊢ ⬕?p P ∗ ⬕?p Q.
+Lemma bare_persistently_if_sep_2 p P Q : ⬕?p P ∗ ⬕?p Q ⊢ ⬕?p (P ∗ Q).
+Proof. destruct p; simpl; auto using bare_persistently_sep_2. Qed.
+Lemma bare_persistently_if_sep `{PositiveBI PROP} p P Q : ⬕?p (P ∗ Q) ⊣⊢ ⬕?p P ∗ ⬕?p Q.
 Proof. destruct p; simpl; auto using bare_persistently_sep. Qed.
 
 Lemma bare_persistently_if_idemp p P : ⬕?p ⬕?p P ⊣⊢ ⬕?p P.
@@ -1211,7 +1215,7 @@ 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_2 -!persistent. Qed.
 
 Global Instance from_option_persistent {A} P (Ψ : A → PROP) (mx : option A) :
   (∀ x, Persistent (Ψ x)) → Persistent P → Persistent (from_option Ψ P mx).
@@ -1294,7 +1298,7 @@ Global Instance bi_persistently_or_homomorphism :
   MonoidHomomorphism bi_or bi_or (≡) (@bi_persistently PROP).
 Proof. split; [split|]; try apply _. apply persistently_or. apply persistently_pure. Qed.
 
-Global Instance bi_persistently_sep_weak_homomorphism :
+Global Instance bi_persistently_sep_weak_homomorphism `{PositiveBI PROP} :
   WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_persistently PROP).
 Proof. split; try apply _. apply persistently_sep. Qed.
 
@@ -1304,7 +1308,7 @@ Proof. split. apply _. apply persistently_emp. Qed.
 
 Global Instance bi_persistently_sep_entails_weak_homomorphism :
   WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_persistently PROP).
-Proof. split; try apply _. intros P Q; by rewrite persistently_sep. Qed.
+Proof. split; try apply _. intros P Q; by rewrite persistently_sep_2. Qed.
 
 Global Instance bi_persistently_sep_entails_homomorphism :
   MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_persistently PROP).
@@ -1421,7 +1425,10 @@ 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 {1}(persistent_persistently_2 P) later_persistently. 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.
 
diff --git a/theories/bi/fractional.v b/theories/bi/fractional.v
index 615d996ab37d1ba75ec6f8228de789412928d98c..38dc36fd00c3b2b416e49e0729f55485bfb9b279 100644
--- a/theories/bi/fractional.v
+++ b/theories/bi/fractional.v
@@ -131,14 +131,14 @@ Section fractional.
     FromSep Q P P.
   Proof. rewrite /FromSep=>-[-> <-] [-> _]. by rewrite Qp_div_2. Qed.
 
-  Global Instance into_sep_fractional p P P1 P2 Φ q1 q2 :
+  Global Instance into_sep_fractional P P1 P2 Φ q1 q2 :
     AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
-    IntoSep p P P1 P2.
+    IntoSep P P1 P2.
   Proof. intros. rewrite /IntoSep [P]fractional_split //. Qed.
 
-  Global Instance into_sep_fractional_half p P Q Φ q :
+  Global Instance into_sep_fractional_half P Q Φ q :
     AsFractional P Φ q → AsFractional Q Φ (q/2) →
-    IntoSep p P Q Q | 100.
+    IntoSep P Q Q | 100.
   Proof. intros. rewrite /IntoSep [P]fractional_half //. Qed.
 
   (* The instance [frame_fractional] can be tried at all the nodes of
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 3e59b2983d08509826fef4073b5c2a303c139c59..982881c769edf0396913a236a3cb9cf1ae527e35 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -99,8 +99,6 @@ Section bi_mixin.
     bi_mixin_wand_intro_r P Q R : (P ∗ Q ⊢ R) → P ⊢ Q -∗ R;
     bi_mixin_wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R;
 
-    bi_mixin_emp_and_sep_assoc_1 Q R : emp ∧ (Q ∗ R) ⊢ (emp ∧ Q) ∗ R;
-
     (* Persistently *)
     bi_mixin_persistently_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q;
     bi_mixin_persistently_idemp_2 P : □ P ⊢ □ □ P;
@@ -401,9 +399,6 @@ Proof. eapply bi_mixin_wand_intro_r, bi_bi_mixin. Qed.
 Lemma wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R.
 Proof. eapply bi_mixin_wand_elim_l', bi_bi_mixin. Qed.
 
-Lemma emp_and_sep_assoc_1 Q R : emp ∧ (Q ∗ R) ⊢ (emp ∧ Q) ∗ R.
-Proof. eapply bi_mixin_emp_and_sep_assoc_1, bi_bi_mixin. Qed.
-
 (* Persistently *)
 Lemma persistently_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q.
 Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index d1bcf824dd1388ffd5e36fb52636d028dfccfb3b..03dffe73a118b476a178367ae93d9ed5ea1c6141 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -185,8 +185,8 @@ Global Instance into_wand_impl_true_true P Q P' :
   FromAssumption true P P' → IntoWand true true (P' → Q) P Q.
 Proof.
   rewrite /FromAssumption /IntoWand /= => <-. apply wand_intro_l.
-  rewrite -{1}(bare_persistently_idemp P) -bare_persistently_sep -persistently_and_sep.
-  by rewrite impl_elim_r bare_persistently_elim.
+  rewrite -{1}(bare_persistently_idemp P) -and_sep_bare_persistently.
+  by rewrite -bare_persistently_and impl_elim_r bare_persistently_elim.
 Qed.
 
 Global Instance into_wand_and_l p q R1 R2 P' Q' :
@@ -266,10 +266,10 @@ Proof. by rewrite /FromSep pure_and sep_and. Qed.
 
 Global Instance from_sep_bare P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (■ P) (■ Q1) (■ Q2).
-Proof. rewrite /FromSep=> <-. by rewrite bare_sep. Qed.
+Proof. rewrite /FromSep=> <-. by rewrite bare_sep_2. Qed.
 Global Instance from_sep_persistently P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (□ P) (□ Q1) (□ Q2).
-Proof. rewrite /FromSep=> <-. by rewrite persistently_sep. Qed.
+Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
 
 Global Instance from_sep_big_sepL_cons {A} (Φ : nat → A → PROP) x l :
   FromSep ([∗ list] k ↦ y ∈ x :: l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l, Φ (S k) y).
@@ -282,11 +282,8 @@ Proof. by rewrite /FromSep big_opL_app. Qed.
 (* IntoAnd *)
 Global Instance into_and_and p P Q : IntoAnd p (P ∧ Q) P Q.
 Proof. by rewrite /IntoAnd bare_persistently_if_and. Qed.
-Global Instance into_and_sep P Q : IntoAnd true (P ∗ Q) P Q.
-Proof.
-    by rewrite /IntoAnd /= bare_persistently_sep -bare_persistently_sep
-               persistently_and_sep.
-Qed.
+Global Instance into_and_sep `{PositiveBI PROP} P Q : IntoAnd true (P ∗ Q) P Q.
+Proof. by rewrite /IntoAnd /= persistently_sep -and_sep_persistently persistently_and. Qed.
 
 Global Instance into_and_pure p φ ψ : @IntoAnd PROP p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. by rewrite /IntoAnd pure_and bare_persistently_if_and. Qed.
@@ -307,55 +304,44 @@ Proof.
 Qed.
 
 (* IntoSep *)
-Global Instance into_sep_sep p P Q : IntoSep p (P ∗ Q) P Q.
-Proof. by rewrite /IntoSep bare_persistently_if_sep. Qed.
-Global Instance into_sep_and P Q : IntoSep true (P ∧ Q) P Q.
-Proof. by rewrite /IntoSep /= persistently_and_sep. Qed.
+Global Instance into_sep_sep P Q : IntoSep (P ∗ Q) P Q.
+Proof. by rewrite /IntoSep. Qed.
 
 Global Instance into_sep_and_persistent_l P P' Q :
-  Persistent P → FromBare P' P → IntoSep false (P ∧ Q) P' Q.
+  Persistent P → FromBare P' P → IntoSep (P ∧ Q) P' Q.
 Proof.
   rewrite /FromBare /IntoSep /=. intros ? <-.
   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'.
+  Persistent Q → FromBare Q' Q → IntoSep (P ∧ Q) P Q'.
 Proof.
   rewrite /FromBare /IntoSep /=. intros ? <-.
   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_1 bare_persistently_if_sep.
-Qed.
 
-Global Instance into_sep_bare p P Q1 Q2 :
-  IntoSep p P Q1 Q2 → IntoSep p (■ P) (■ Q1) (■ Q2).
-Proof.
-  rewrite /IntoSep /=. destruct p; simpl.
-  - by rewrite -bare_sep !persistently_bare.
-  - intros ->. by rewrite bare_sep.
-Qed.
-Global Instance into_sep_persistently p P Q1 Q2 :
-  IntoSep p P Q1 Q2 → IntoSep p (□ P) (□ Q1) (□ Q2).
-Proof.
-  rewrite /IntoSep /=. destruct p; simpl.
-  - by rewrite -persistently_sep !persistently_idemp.
-  - intros ->. by rewrite persistently_sep.
-Qed.
+Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
+Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.
+
+Global Instance into_sep_bare `{PositiveBI PROP} P Q1 Q2 :
+  IntoSep P Q1 Q2 → IntoSep (■ P) (■ Q1) (■ Q2).
+Proof. rewrite /IntoSep /= => ->. by rewrite bare_sep. Qed.
+Global Instance into_sep_persistently `{PositiveBI PROP} P Q1 Q2 :
+  IntoSep P Q1 Q2 → IntoSep (□ P) (□ Q1) (□ Q2).
+Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
 
 (* We use [IsCons] and [IsApp] to make sure that [frame_big_sepL_cons] and
 [frame_big_sepL_app] cannot be applied repeatedly often when having
 [ [∗ list] k ↦ x ∈ ?e, Φ k x] with [?e] an evar. *)
-Global Instance into_sep_big_sepL_cons {A} p (Φ : nat → A → PROP) l x l' :
+Global Instance into_sep_big_sepL_cons {A} (Φ : nat → A → PROP) l x l' :
   IsCons l x l' →
-  IntoSep p ([∗ list] k ↦ y ∈ l, Φ k y)
+  IntoSep ([∗ list] k ↦ y ∈ l, Φ k y)
     (Φ 0 x) ([∗ list] k ↦ y ∈ l', Φ (S k) y).
 Proof. rewrite /IsCons=>->. by rewrite /IntoSep big_sepL_cons. Qed.
-Global Instance into_sep_big_sepL_app {A} p (Φ : nat → A → PROP) l l1 l2 :
+Global Instance into_sep_big_sepL_app {A} (Φ : nat → A → PROP) l l1 l2 :
   IsApp l l1 l2 →
-  IntoSep p ([∗ list] k ↦ y ∈ l, Φ k y)
+  IntoSep ([∗ 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 /IntoSep big_sepL_app. Qed.
 
@@ -499,7 +485,7 @@ Global Instance frame_sep_persistent_l R P1 P2 Q1 Q2 Q' :
   Frame true R (P1 ∗ P2) Q' | 9.
 Proof.
   rewrite /Frame /MaybeFrame /MakeSep /= => <- <- <-.
-  rewrite {1}(persistently_sep_dup R) bare_sep. solve_sep_entails.
+  rewrite {1}(bare_persistently_sep_dup R). solve_sep_entails.
 Qed.
 Global Instance frame_sep_l R P1 P2 Q Q' :
   Frame false R P1 Q → MakeSep Q P2 Q' → Frame false R (P1 ∗ P2) Q' | 9.
@@ -602,7 +588,10 @@ Proof. by rewrite /MakeBare. Qed.
 
 Global Instance frame_bare R P Q Q' :
   Frame true R P Q → MakeBare Q Q' → Frame true R (■ P) Q'.
-Proof. rewrite /Frame /MakeBare=> <- <- /=. by rewrite bare_sep bare_idemp. Qed.
+Proof.
+  rewrite /Frame /MakeBare=> <- <- /=.
+  by rewrite -{1}bare_idemp bare_sep_2.
+Qed.
 
 Class MakePersistently (P Q : PROP) := make_persistently : □ P ⊣⊢ Q.
 Arguments MakePersistently _%I _%I.
@@ -616,9 +605,9 @@ Proof. by rewrite /MakePersistently. Qed.
 Global Instance frame_persistently R P Q Q' :
   Frame true R P Q → MakePersistently Q Q' → Frame true R (□ P) Q'.
 Proof.
-  rewrite /Frame /MakePersistently=> <- <- /=.
-  by rewrite -persistently_and_bare_sep_l persistently_sep persistently_bare
-             persistently_idemp -persistently_and_sep_l_1.
+  rewrite /Frame /MakePersistently=> <- <- /=. rewrite -persistently_and_bare_sep_l.
+  by rewrite -persistently_sep_2 -persistently_and_sep_l_1 persistently_bare
+              persistently_idemp.
 Qed.
 
 Global Instance frame_exist {A} p R (Φ Ψ : A → PROP) :
@@ -722,24 +711,15 @@ Proof.
 Qed.
 
 (* IntoSep *)
-Global Instance into_sep_later p P Q1 Q2 :
-  IntoSep p P Q1 Q2 → IntoSep p (▷ P) (▷ Q1) (▷ Q2).
-Proof.
-  rewrite /IntoSep=> HP. apply bare_persistently_if_intro'.
-  by rewrite bare_persistently_if_later HP bare_persistently_if_elim later_sep.
-Qed.
-Global Instance into_sep_laterN n p P Q1 Q2 :
-  IntoSep p P Q1 Q2 → IntoSep p (▷^n P) (▷^n Q1) (▷^n Q2).
-Proof.
-  rewrite /IntoSep=> HP. apply bare_persistently_if_intro'.
-  by rewrite bare_persistently_if_laterN HP bare_persistently_if_elim laterN_sep.
-Qed.
-Global Instance into_sep_except_0 p P Q1 Q2 :
-  IntoSep p P Q1 Q2 → IntoSep p (◇ P) (◇ Q1) (◇ Q2).
-Proof.
-  rewrite /IntoSep=> HP. apply bare_persistently_if_intro'.
-  by rewrite bare_persistently_if_except_0 HP bare_persistently_if_elim except_0_sep.
-Qed.
+Global Instance into_sep_later P Q1 Q2 :
+  IntoSep P Q1 Q2 → IntoSep (▷ P) (▷ Q1) (▷ Q2).
+Proof. rewrite /IntoSep=> ->. by rewrite later_sep. Qed.
+Global Instance into_sep_laterN n P Q1 Q2 :
+  IntoSep P Q1 Q2 → IntoSep (▷^n P) (▷^n Q1) (▷^n Q2).
+Proof. rewrite /IntoSep=> ->. by rewrite laterN_sep. Qed.
+Global Instance into_sep_except_0 P Q1 Q2 :
+  IntoSep P Q1 Q2 → IntoSep (◇ P) (◇ Q1) (◇ Q2).
+Proof. rewrite /IntoSep=> ->. by rewrite except_0_sep. Qed.
 
 (* FromOr *)
 Global Instance from_or_later P Q1 Q2 :
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 1f620fb707f9d2a8d17c80d338cee1a18e603c93..d44d6d5f48fbfd3895496c2b593e591069077325 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -121,11 +121,11 @@ Arguments IntoAnd {_} _ _%I _%I _%I : simpl never.
 Arguments into_and {_} _ _%I _%I _%I {_}.
 Hint Mode IntoAnd + + ! - - : typeclass_instances.
 
-Class IntoSep {PROP : bi} (p : bool) (P Q1 Q2 : PROP) :=
-  into_sep : ⬕?p P ⊢ ⬕?p (Q1 ∗ Q2).
-Arguments IntoSep {_} _ _%I _%I _%I : simpl never.
-Arguments into_sep {_} _ _%I _%I _%I {_}.
-Hint Mode IntoAnd + + ! - - : typeclass_instances.
+Class IntoSep {PROP : bi} (P Q1 Q2 : PROP) :=
+  into_sep : P ⊢ Q1 ∗ Q2.
+Arguments IntoSep {_} _%I _%I _%I : simpl never.
+Arguments into_sep {_} _%I _%I _%I {_}.
+Hint Mode IntoSep + ! - - : typeclass_instances.
 
 Class FromOr {PROP : bi} (P Q1 Q2 : PROP) := from_or : Q1 ∨ Q2 ⊢ P.
 Arguments FromOr {_} _%I _%I _%I : simpl never.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 428cda55c65c9b1172f9e818845ac4bac01f0cd8..817edd512e3e8d298906736c73e56f0807af7a0c 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -22,7 +22,7 @@ Record envs_wf {PROP} (Δ : envs PROP) := {
 }.
 
 Coercion of_envs {PROP} (Δ : envs PROP) : PROP :=
-  (⌜envs_wf Δ⌝ ∧ ⬕ [∗] env_persistent Δ ∗ [∗] env_spatial Δ)%I.
+  (⌜envs_wf Δ⌝ ∧ ⬕ [∧] env_persistent Δ ∗ [∗] env_spatial Δ)%I.
 Instance: Params (@of_envs) 1.
 Arguments of_envs : simpl never.
 
@@ -126,7 +126,7 @@ Implicit Types Δ : envs PROP.
 Implicit Types P Q : PROP.
 
 Lemma of_envs_eq Δ :
-  of_envs Δ = (⌜envs_wf Δ⌝ ∧ ⬕ [∗] env_persistent Δ ∗ [∗] env_spatial Δ)%I.
+  of_envs Δ = (⌜envs_wf Δ⌝ ∧ ⬕ [∧] env_persistent Δ ∗ [∗] env_spatial Δ)%I.
 Proof. done. Qed.
 
 Lemma envs_lookup_delete_Some Δ Δ' i p P :
@@ -145,7 +145,8 @@ Proof.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
   - rewrite pure_True ?left_id; last (destruct Hwf; constructor;
       naive_solver eauto using env_delete_wf, env_delete_fresh).
-    by rewrite (env_lookup_perm Γp) //= bare_persistently_sep -assoc.
+    rewrite (env_lookup_perm Γp) //= bare_persistently_and.
+    by rewrite and_sep_bare_persistently -assoc.
   - destruct (Γs !! i) eqn:?; simplify_eq/=.
     rewrite pure_True ?left_id; last (destruct Hwf; constructor;
       naive_solver eauto using env_delete_wf, env_delete_fresh).
@@ -165,7 +166,7 @@ Proof.
   rewrite /envs_lookup /of_envs=>?. apply pure_elim_l=> Hwf.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
   - rewrite pure_True // left_id.
-    rewrite (env_lookup_perm Γp) //= bare_persistently_sep.
+    rewrite (env_lookup_perm Γp) //= bare_persistently_and and_sep_bare_persistently.
     cancel [⬕ P]%I. apply wand_intro_l. solve_sep_entails.
   - destruct (Γs !! i) eqn:?; simplify_eq/=.
     rewrite (env_lookup_perm Γs) //=. rewrite pure_True // left_id.
@@ -177,14 +178,15 @@ Lemma envs_lookup_delete_sound Δ Δ' i p P :
 Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound. Qed.
 
 Lemma envs_lookup_delete_list_sound Δ Δ' js rp p Ps :
-  envs_lookup_delete_list js rp Δ = Some (p,Ps,Δ') → Δ ⊢ ⬕?p [∗] Ps ∗ Δ'.
+  envs_lookup_delete_list js rp Δ = Some (p,Ps,Δ') →
+  Δ ⊢ ⬕?p [∗] Ps ∗ Δ'.
 Proof.
   revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
   { by rewrite bare_persistently_emp left_id. }
   destruct (envs_lookup_delete j Δ) as [[[q1 P] Δ']|] eqn:Hj; simplify_eq/=.
   apply envs_lookup_delete_Some in Hj as [Hj ->].
   destruct (envs_lookup_delete_list js rp _) as [[[q2 Ps'] ?]|] eqn:?; simplify_eq/=.
-  rewrite bare_persistently_if_sep -assoc. destruct q1; simpl.
+  rewrite -bare_persistently_if_sep_2 -assoc. destruct q1; simpl.
   - destruct rp.
     + rewrite envs_lookup_sound //; simpl.
       by rewrite IH // (bare_persistently_bare_persistently_if q2).
@@ -215,14 +217,15 @@ Proof.
   - apply and_intro; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
       intros j; destruct (strings.string_beq_reflect j i); naive_solver.
-    + by rewrite bare_persistently_sep assoc.
+    + by rewrite bare_persistently_and and_sep_bare_persistently assoc.
   - apply and_intro; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
       intros j; destruct (strings.string_beq_reflect j i); naive_solver.
     + solve_sep_entails.
 Qed.
 
-Lemma envs_app_sound Δ Δ' p Γ : envs_app p Γ Δ = Some Δ' → Δ ⊢ ⬕?p [∗] Γ -∗ Δ'.
+Lemma envs_app_sound Δ Δ' p Γ :
+  envs_app p Γ Δ = Some Δ' → Δ ⊢ (if p then ⬕ [∧] Γ else [∗] Γ) -∗ Δ'.
 Proof.
   rewrite /of_envs /envs_app=> ?; apply pure_elim_l=> Hwf.
   destruct Δ as [Γp Γs], p; simplify_eq/=.
@@ -233,7 +236,8 @@ Proof.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       naive_solver eauto using env_app_fresh.
     + rewrite (env_app_perm _ _ Γp') //.
-      rewrite big_opL_app bare_persistently_sep. solve_sep_entails.
+      rewrite big_opL_app bare_persistently_and and_sep_bare_persistently.
+      solve_sep_entails.
   - destruct (env_app Γ Γp) eqn:Happ,
       (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
     apply wand_intro_l, and_intro; [apply pure_intro|].
@@ -243,9 +247,13 @@ Proof.
     + rewrite (env_app_perm _ _ Γs') // big_opL_app. solve_sep_entails.
 Qed.
 
+Lemma envs_app_singleton_sound Δ Δ' p j Q :
+  envs_app p (Esnoc Enil j Q) Δ = Some Δ' → Δ ⊢ ⬕?p Q -∗ Δ'.
+Proof. move=> /envs_app_sound. destruct p; by rewrite /= right_id. Qed.
+
 Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
   envs_simple_replace i p Γ Δ = Some Δ' →
-  envs_delete i p Δ ⊢ ⬕?p [∗] Γ -∗ Δ'.
+  envs_delete i p Δ ⊢ (if p then ⬕ [∧] Γ else [∗] Γ) -∗ Δ'.
 Proof.
   rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
   apply pure_elim_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
@@ -256,7 +264,8 @@ Proof.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
     + rewrite (env_replace_perm _ _ Γp') //.
-      rewrite big_opL_app bare_persistently_sep. solve_sep_entails.
+      rewrite big_opL_app bare_persistently_and and_sep_bare_persistently.
+      solve_sep_entails.
   - destruct (env_app Γ Γp) eqn:Happ,
       (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
     apply wand_intro_l, and_intro; [apply pure_intro|].
@@ -266,24 +275,49 @@ Proof.
     + rewrite (env_replace_perm _ _ Γs') // big_opL_app. solve_sep_entails.
 Qed.
 
+Lemma envs_simple_replace_singleton_sound' Δ Δ' i p j Q :
+  envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' →
+  envs_delete i p Δ ⊢ ⬕?p Q -∗ Δ'.
+Proof. move=> /envs_simple_replace_sound'. destruct p; by rewrite /= right_id. Qed.
+
 Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
   envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
-  Δ ⊢ ⬕?p P ∗ (⬕?p [∗] Γ -∗ Δ').
+  Δ ⊢ ⬕?p P ∗ ((if p then ⬕ [∧] Γ else [∗] Γ) -∗ Δ').
 Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.
 
+Lemma envs_simple_replace_singleton_sound Δ Δ' i p P j Q :
+  envs_lookup i Δ = Some (p,P) →
+  envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' →
+  Δ ⊢ ⬕?p P ∗ (⬕?p Q -∗ Δ').
+Proof.
+  intros. by rewrite envs_lookup_sound// envs_simple_replace_singleton_sound'//.
+Qed.
+
 Lemma envs_replace_sound' Δ Δ' i p q Γ :
-  envs_replace i p q Γ Δ = Some Δ' → envs_delete i p Δ ⊢ ⬕?q [∗] Γ -∗ Δ'.
+  envs_replace i p q Γ Δ = Some Δ' →
+  envs_delete i p Δ ⊢ (if q then ⬕ [∧] Γ else [∗] Γ) -∗ Δ'.
 Proof.
   rewrite /envs_replace; destruct (eqb _ _) eqn:Hpq.
   - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
   - apply envs_app_sound.
 Qed.
 
+Lemma envs_replace_singleton_sound' Δ Δ' i p q j Q :
+  envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' →
+  envs_delete i p Δ ⊢ ⬕?q Q -∗ Δ'.
+Proof. move=> /envs_replace_sound'. destruct q; by rewrite /= ?right_id. Qed.
+
 Lemma envs_replace_sound Δ Δ' i p q P Γ :
   envs_lookup i Δ = Some (p,P) → envs_replace i p q Γ Δ = Some Δ' →
-  Δ ⊢ ⬕?p P ∗ (⬕?q [∗] Γ -∗ Δ').
+  Δ ⊢ ⬕?p P ∗ ((if q then ⬕ [∧] Γ else [∗] Γ) -∗ Δ').
 Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.
 
+Lemma envs_replace_singleton_sound Δ Δ' i p q P j Q :
+  envs_lookup i Δ = Some (p,P) →
+  envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' →
+  Δ ⊢ ⬕?p P ∗ (⬕?q Q -∗ Δ').
+Proof. intros. by rewrite envs_lookup_sound// envs_replace_singleton_sound'//. Qed.
+
 Lemma envs_lookup_envs_clear_spatial Δ j :
   envs_lookup j (envs_clear_spatial Δ)
   = '(p,P) ← envs_lookup j Δ; if p then Some (p,P) else None.
@@ -396,7 +430,7 @@ Proof. by constructor. Qed.
 (** * Adequacy *)
 Lemma tac_adequate P : (Envs Enil Enil ⊢ P) → P.
 Proof.
-  intros <-. rewrite /of_envs /= bare_persistently_emp left_id.
+  intros <-. rewrite /of_envs /= persistently_True_emp bare_persistently_emp left_id.
   apply and_intro=> //. apply pure_intro; repeat constructor.
 Qed.
 
@@ -437,8 +471,8 @@ Lemma tac_rename Δ Δ' i j p P Q :
   envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros. rewrite envs_simple_replace_sound //.
-  destruct p; simpl; by rewrite right_id wand_elim_r.
+  intros. rewrite envs_simple_replace_singleton_sound //.
+  by rewrite wand_elim_r.
 Qed.
 
 Lemma tac_clear Δ Δ' i p P Q :
@@ -501,33 +535,44 @@ Lemma tac_persistent Δ Δ' i p P P' Q :
   envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros ???? <-. rewrite envs_replace_sound //; simpl.
-  rewrite right_id. apply wand_elim_r', wand_mono=> //. destruct p; simpl.
+  intros ???? <-. rewrite envs_replace_singleton_sound //; simpl.
+  apply wand_elim_r', wand_mono=> //. destruct p; simpl.
   - by rewrite -(into_persistent _ P).
   - by rewrite -(into_persistent _ P) /= affine_bare.
 Qed.
 
 (** * Implication and wand *)
+Lemma envs_app_singleton_sound_foo Δ Δ' p j Q :
+  envs_app p (Esnoc Enil j Q) Δ = Some Δ' → Δ ∗ ⬕?p Q ⊢ Δ'.
+Proof. intros. apply wand_elim_l'. eapply envs_app_singleton_sound. eauto. Qed.
+
 Lemma tac_impl_intro Δ Δ' i P Q :
   (if env_spatial_is_nil Δ then TCTrue else Persistent P) →
   envs_app false (Esnoc Enil i P) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ P → Q.
 Proof.
   intros ?? <-. destruct (env_spatial_is_nil Δ) eqn:?.
-  - rewrite (env_spatial_is_nil_bare_persistently Δ) // envs_app_sound //; simpl.
-    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_1 right_id wand_elim_r.
+  - rewrite (env_spatial_is_nil_bare_persistently Δ) //; simpl. apply impl_intro_l.
+    rewrite envs_app_singleton_sound //; simpl.
+    by rewrite bare_elim persistently_and_bare_sep_r bare_persistently_elim wand_elim_r.
+  - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
+    by rewrite persistent_and_sep_1 wand_elim_r.
 Qed.
 Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
   IntoPersistent false P P' →
   envs_app true (Esnoc Enil i P') Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ P → Q.
 Proof.
-  intros ?? <-. rewrite envs_app_sound //; simpl. apply impl_intro_l.
+  intros ?? <-. rewrite envs_app_singleton_sound //; simpl. apply impl_intro_l.
   rewrite (_ : P = â–¡?false P)%I // (into_persistent false P).
-  by rewrite right_id persistently_and_bare_sep_l wand_elim_r.
+  by rewrite persistently_and_bare_sep_l wand_elim_r.
+Qed.
+Lemma tac_pure_impl_intro Δ (φ ψ : Prop) :
+  (φ → Δ ⊢ ⌜ψ⌝) → Δ ⊢ ⌜φ → ψ⌝.
+Proof. intros. rewrite pure_impl. by apply impl_intro_l, pure_elim_l. Qed.
+Lemma tac_impl_intro_pure Δ P φ Q : IntoPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ P → Q.
+Proof.
+  intros. apply impl_intro_l. rewrite (into_pure P). by apply pure_elim_l.
 Qed.
 
 Lemma tac_impl_intro_drop Δ P Q : (Δ ⊢ Q) → Δ ⊢ P → Q.
@@ -544,9 +589,16 @@ Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
   envs_app true (Esnoc Enil i P') Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ P -∗ Q.
 Proof.
-  intros ??? <-. rewrite envs_app_sound //; simpl.
-  rewrite right_id. apply wand_mono=>//.
-  by rewrite -(into_persistent _ P) /= affine_bare.
+  intros ??? <-. rewrite envs_app_singleton_sound //; simpl.
+  apply wand_mono=>//. by rewrite -(into_persistent _ P) /= affine_bare.
+Qed.
+Lemma tac_wand_intro_pure Δ P φ Q :
+  IntoPure P φ →
+  Affine P →
+  (φ → Δ ⊢ Q) → Δ ⊢ P -∗ Q.
+Proof.
+  intros. apply wand_intro_l. rewrite -(affine_bare P) (into_pure P).
+  rewrite -persistent_and_bare_sep_l. by apply pure_elim_l.
 Qed.
 Lemma tac_wand_intro_drop Δ P Q :
   TCOr (Affine P) (Absorbing Q) →
@@ -568,13 +620,14 @@ Lemma tac_specialize Δ Δ' Δ'' i p j q P1 P2 R Q :
   (Δ'' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
-  - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
+  - rewrite envs_lookup_persistent_sound //.
+    rewrite envs_simple_replace_singleton_sound //; simpl.
     rewrite -bare_persistently_if_idemp -bare_persistently_idemp into_wand /=.
-    rewrite assoc (bare_persistently_bare_persistently_if q) -bare_persistently_if_sep wand_elim_r.
-    by rewrite right_id wand_elim_r.
+    rewrite assoc (bare_persistently_bare_persistently_if q).
+    by rewrite bare_persistently_if_sep_2 wand_elim_r wand_elim_r.
   - rewrite envs_lookup_sound //; simpl.
-    rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
-    by rewrite into_wand /= assoc wand_elim_r right_id wand_elim_r.
+    rewrite envs_lookup_sound // (envs_replace_singleton_sound' _ Δ'') //; simpl.
+    by rewrite into_wand /= assoc wand_elim_r wand_elim_r.
 Qed.
 
 Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
@@ -590,9 +643,9 @@ Proof.
   destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
     destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
   rewrite envs_lookup_sound // envs_split_sound //.
-  rewrite (envs_app_sound Δ2) //; simpl.
+  rewrite (envs_app_singleton_sound Δ2) //; simpl.
   rewrite HP1 into_wand /= -(elim_modal P1' P1 Q Q). cancel [P1'].
-  apply wand_intro_l. by rewrite assoc right_id !wand_elim_r.
+  apply wand_intro_l. by rewrite assoc !wand_elim_r.
 Qed.
 
 Lemma tac_unlock P Q : (P ⊢ Q) → P ⊢ locked Q.
@@ -619,10 +672,10 @@ Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
   envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' →
   φ → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros. rewrite envs_simple_replace_sound //; simpl.
+  intros. rewrite envs_simple_replace_singleton_sound //; simpl.
   rewrite -bare_persistently_if_idemp into_wand /= -(from_pure P1).
   rewrite pure_True // persistently_pure bare_True_emp bare_emp.
-  by rewrite emp_wand right_id wand_elim_r.
+  by rewrite emp_wand wand_elim_r.
 Qed.
 
 Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P2 R Q :
@@ -635,10 +688,10 @@ Proof.
   intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
   rewrite envs_lookup_sound //.
   rewrite -(idemp bi_and (envs_delete _ _ _)).
-  rewrite {2}envs_simple_replace_sound' //; rewrite /= right_id.
+  rewrite {2}envs_simple_replace_singleton_sound' //; simpl.
   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.
+  rewrite (bare_persistently_bare_persistently_if q) bare_persistently_if_sep_2.
   by rewrite into_wand wand_elim_l wand_elim_r.
 Qed.
 
@@ -646,15 +699,16 @@ Lemma tac_specialize_persistent_helper Δ Δ'' j q P R R' Q :
   envs_lookup j Δ = Some (q,P) →
   (Δ ⊢ R) →
   IntoPersistent false R R' →
-  (if q then TCTrue else Affine R) →
+  (if q then TCTrue else TCAnd (PositiveBI PROP) (Affine R)) →
   envs_replace j q true (Esnoc Enil j R') Δ = Some Δ'' →
   (Δ'' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros ? HR ??? <-. rewrite -(idemp bi_and Δ) {1}HR.
-  rewrite envs_replace_sound //; rewrite /= right_id. destruct q; simpl.
+  intros ? HR ? Hpos ? <-. rewrite -(idemp bi_and Δ) {1}HR.
+  rewrite envs_replace_singleton_sound //; destruct q; simpl.
   - rewrite (_ : R = â–¡?false R)%I // (into_persistent _ R).
     by rewrite sep_elim_r persistently_and_bare_sep_l wand_elim_r.
-  - rewrite -(affine_bare R) (_ : R = â–¡?false R)%I // (into_persistent _ R).
+  - destruct Hpos.
+    rewrite -(affine_bare R) (_ : R = â–¡?false R)%I // (into_persistent _ R).
     rewrite bare_and_r -bare_and_l bare_sep sep_elim_r bare_elim.
     by rewrite persistently_and_bare_sep_l wand_elim_r.
 Qed.
@@ -697,8 +751,7 @@ Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P P' Q :
   (Δ1 ⊢ P') → (Δ2' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ??? HP HQ. rewrite envs_split_sound //.
-  rewrite (envs_app_sound Δ2) //; simpl.
-  by rewrite right_id HP HQ.
+  rewrite (envs_app_singleton_sound Δ2) //; simpl. by rewrite HP HQ.
 Qed.
 
 Lemma tac_assert_persistent Δ Δ1 Δ2 Δ' lr js j P P' Q :
@@ -711,8 +764,7 @@ Proof.
   intros ???? HP <-. rewrite -(idemp bi_and Δ) {1}envs_split_sound //.
   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.
+  rewrite envs_app_singleton_sound //; simpl. by rewrite wand_elim_r.
 Qed.
 
 Lemma tac_assert_pure Δ Δ' j P P' φ Q :
@@ -721,8 +773,8 @@ Lemma tac_assert_pure Δ Δ' j P P' φ Q :
   envs_app false (Esnoc Enil j P') Δ = Some Δ' →
   φ → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros ???? <-. rewrite envs_app_sound //; simpl.
-  rewrite right_id -(from_bare P') -(from_pure P) pure_True //.
+  intros ???? <-. rewrite envs_app_singleton_sound //; simpl.
+  rewrite -(from_bare P') -(from_pure P) pure_True //.
   by rewrite bare_True_emp bare_emp emp_wand.
 Qed.
 
@@ -731,8 +783,8 @@ Lemma tac_pose_proof Δ Δ' j P Q :
   envs_app true (Esnoc Enil j P) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros HP ? <-. rewrite envs_app_sound //; simpl.
-  by rewrite right_id -HP bare_persistently_emp emp_wand.
+  intros HP ? <-. rewrite envs_app_singleton_sound //; simpl.
+  by rewrite -HP bare_persistently_emp emp_wand.
 Qed.
 
 Lemma tac_pose_proof_hyp Δ Δ' Δ'' i p j P Q :
@@ -741,10 +793,10 @@ Lemma tac_pose_proof_hyp Δ Δ' Δ'' i p j P Q :
   (Δ'' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros [? ->]%envs_lookup_delete_Some ? <-. destruct p.
-  - rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
-    by rewrite right_id wand_elim_r.
-  - rewrite envs_lookup_sound // envs_app_sound //; simpl.
-    by rewrite right_id wand_elim_r.
+  - rewrite envs_lookup_persistent_sound // envs_app_singleton_sound //; simpl.
+    by rewrite wand_elim_r.
+  - rewrite envs_lookup_sound // envs_app_singleton_sound //; simpl.
+    by rewrite wand_elim_r.
 Qed.
 
 Lemma tac_apply Δ Δ' i p R P1 P2 :
@@ -783,8 +835,8 @@ Lemma tac_rewrite_in Δ i p Pxy j q P (lr : bool) Q :
 Proof.
   intros ?? A Δ' x y Φ HPxy HP ?? <-.
   rewrite -(idemp bi_and Δ) {2}(envs_lookup_sound _ i) //.
-  rewrite (envs_simple_replace_sound _ _ j) //; simpl.
-  rewrite HP right_id HPxy (bare_persistently_if_elim _ (_ ≡ _)%I) sep_elim_l.
+  rewrite (envs_simple_replace_singleton_sound _ _ j) //; simpl.
+  rewrite HP HPxy (bare_persistently_if_elim _ (_ ≡ _)%I) sep_elim_l.
   rewrite persistent_and_bare_sep_r -assoc. apply wand_elim_r'.
   rewrite -persistent_and_bare_sep_r. apply impl_elim_r'. destruct lr.
   - apply (internal_eq_rewrite x y (λ y, ⬕?q Φ y -∗ Δ')%I). solve_proper.
@@ -825,18 +877,20 @@ Lemma tac_combine Δ1 Δ2 Δ3 js p Ps j P Q :
   (Δ3 ⊢ Q) → Δ1 ⊢ Q.
 Proof.
   intros ??? <-. rewrite envs_lookup_delete_list_sound //.
-  rewrite from_seps. rewrite envs_app_sound //; simpl.
-  by rewrite right_id wand_elim_r.
+  rewrite from_seps. rewrite envs_app_singleton_sound //; simpl.
+  by rewrite wand_elim_r.
 Qed.
 
 (** * Conjunction/separating conjunction elimination *)
 Lemma tac_and_destruct Δ Δ' i p j1 j2 P P1 P2 Q :
-  envs_lookup i Δ = Some (p, P) → IntoSep p P P1 P2 →
+  envs_lookup i Δ = Some (p, P) →
+  (if p then IntoAnd true P P1 P2 else IntoSep P P1 P2) →
   envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros. rewrite envs_simple_replace_sound //; simpl.
-  by rewrite (into_sep _ P) right_id -(comm _ P1) wand_elim_r.
+  intros. rewrite envs_simple_replace_sound //; simpl. destruct p.
+  - by rewrite (into_and _ P) /= right_id -(comm _ P1) wand_elim_r.
+  - by rewrite (into_sep P) right_id -(comm _ P1) wand_elim_r.
 Qed.
 
 (* Using this tactic, one can destruct a (non-separating) conjunction in the
@@ -844,23 +898,25 @@ spatial context as long as one of the conjuncts is thrown away. It corresponds
 to the principle of "external choice" in linear logic. *)
 Lemma tac_and_destruct_choice Δ Δ' i p (lr : bool) j P P1 P2 Q :
   envs_lookup i Δ = Some (p, P) →
-  TCOr (IntoAnd p P P1 P2) (TCAnd (IntoSep p P P1 P2)
-    (if p then TCTrue
-     else if lr then TCOr (Affine P2) (Absorbing Q)
-     else TCOr (Affine P1) (Absorbing Q))) →
+  (if p then IntoAnd p P P1 P2 : Type else
+    TCOr (IntoAnd p P P1 P2) (TCAnd (IntoSep P P1 P2)
+      (if lr then TCOr (Affine P2) (Absorbing Q)
+       else TCOr (Affine P1) (Absorbing Q)))) →
   envs_simple_replace i p (Esnoc Enil j (if lr then P1 else P2)) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros ? HP ? HQ. rewrite envs_simple_replace_sound //; simpl.
+  intros ? HP ? HQ. rewrite envs_simple_replace_singleton_sound //; simpl.
+  destruct p.
+  { rewrite (into_and _ P) HQ. destruct lr; simpl.
+    - by rewrite and_elim_l wand_elim_r.
+    - by rewrite and_elim_r wand_elim_r. }
   destruct HP as [?|[??]].
-  - rewrite (into_and _ P) right_id  HQ. destruct lr.
-    + by rewrite and_elim_l wand_elim_r.
-    + by rewrite and_elim_r wand_elim_r.
-  - rewrite (into_sep _ P) right_id HQ bare_persistently_if_sep. destruct p, lr; simpl.
-    + by rewrite (sep_elim_l (⬕ P1)%I) wand_elim_r.
-    + by rewrite (sep_elim_r (⬕ P1)%I) wand_elim_r.
-    + by rewrite (comm _ P1) -assoc wand_elim_r sep_elim_r.
-    + by rewrite -assoc wand_elim_r sep_elim_r.
+  { rewrite (into_and _ P) HQ. destruct lr; simpl.
+    - by rewrite and_elim_l wand_elim_r.
+    - by rewrite and_elim_r wand_elim_r. }
+  rewrite (into_sep P) HQ. destruct lr; simpl.
+  - by rewrite (comm _ P1) -assoc wand_elim_r sep_elim_r.
+  - by rewrite -assoc wand_elim_r sep_elim_r.
 Qed.
 
 (** * Framing *)
@@ -895,10 +951,10 @@ Lemma tac_or_destruct Δ Δ1 Δ2 i p j1 j2 P P1 P2 Q :
 Proof.
   intros ???? HP1 HP2. rewrite envs_lookup_sound //.
   rewrite (into_or P) bare_persistently_if_or sep_or_r; apply or_elim.
-  - rewrite (envs_simple_replace_sound' _ Δ1) //.
-    by rewrite /= right_id wand_elim_r.
-  - rewrite (envs_simple_replace_sound' _ Δ2) //.
-    by rewrite /= right_id wand_elim_r.
+  - rewrite (envs_simple_replace_singleton_sound' _ Δ1) //.
+    by rewrite wand_elim_r.
+  - rewrite (envs_simple_replace_singleton_sound' _ Δ2) //.
+    by rewrite wand_elim_r.
 Qed.
 
 (** * Forall *)
@@ -915,8 +971,8 @@ Lemma tac_forall_specialize {A} Δ Δ' i p P (Φ : A → PROP) Q :
     (Δ' ⊢ Q)) →
   Δ ⊢ Q.
 Proof.
-  intros ?? (x&?&?). rewrite envs_simple_replace_sound //; simpl.
-  by rewrite right_id (into_forall P) (forall_elim x) wand_elim_r.
+  intros ?? (x&?&?). rewrite envs_simple_replace_singleton_sound //; simpl.
+  by rewrite (into_forall P) (forall_elim x) wand_elim_r.
 Qed.
 
 Lemma tac_forall_revert {A} Δ (Φ : A → PROP) :
@@ -937,7 +993,7 @@ Proof.
   intros ?? HΦ. rewrite envs_lookup_sound //.
   rewrite (into_exist P) bare_persistently_if_exist sep_exist_r.
   apply exist_elim=> a; destruct (HΦ a) as (Δ'&?&?).
-  rewrite envs_simple_replace_sound' //; simpl. by rewrite right_id wand_elim_r.
+  rewrite envs_simple_replace_singleton_sound' //; simpl. by rewrite wand_elim_r.
 Qed.
 
 (** * Modalities *)
@@ -950,8 +1006,8 @@ Lemma tac_modal_elim Δ Δ' i p P' P Q Q' :
   envs_replace i p false (Esnoc Enil i P') Δ = Some Δ' →
   (Δ' ⊢ Q') → Δ ⊢ Q.
 Proof.
-  intros ??? HΔ. rewrite envs_replace_sound //; simpl.
-  rewrite right_id HΔ bare_persistently_if_elim. by apply elim_modal.
+  intros ??? HΔ. rewrite envs_replace_singleton_sound //; simpl.
+  rewrite HΔ bare_persistently_if_elim. by apply elim_modal.
 Qed.
 End bi_tactics.
 
@@ -990,7 +1046,7 @@ Proof.
   - apply pure_mono; destruct 1; constructor;
       naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
   - apply bare_mono, persistently_mono.
-    induction Hp; rewrite /= ?laterN_sep. apply laterN_intro. by apply sep_mono.
+    induction Hp; rewrite /= ?laterN_and. apply laterN_intro. by apply and_mono.
   - induction Hs; rewrite /= ?laterN_sep. apply laterN_intro. by apply sep_mono.
 Qed.
 
@@ -1006,8 +1062,8 @@ Proof.
   intros ?? HQ. rewrite (env_spatial_is_nil_bare_persistently Δ) //.
   rewrite -(persistently_and_emp_elim Q). apply and_intro; first apply: affine.
   rewrite -(löb (□ Q)%I) later_persistently. apply impl_intro_l.
-  rewrite envs_app_sound //; simpl; rewrite HQ right_id.
-  rewrite persistently_and_bare_sep_l -{1}bare_persistently_idemp -bare_persistently_sep.
+  rewrite envs_app_singleton_sound //; simpl; rewrite HQ.
+  rewrite persistently_and_bare_sep_l -{1}bare_persistently_idemp bare_persistently_sep_2.
   by rewrite wand_elim_r bare_elim.
 Qed.
 End sbi_tactics.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 03f23388f237f55ea3027668b2b09048cc15b45e..51eb5eabd7d114497d4bd28ddcc4cc40a4d766b8 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -531,8 +531,9 @@ Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) :=
       quantifiers are instantiated. *)
       let pat := spec_pat.parse pat in
       lazymatch eval compute in
-        (bool_decide (pat ≠ []) && p && negb (existsb spec_pat_modal pat)) with
+        (p && bool_decide (pat ≠ []) && negb (existsb spec_pat_modal pat)) with
       | true =>
+         (* FIXME: do something reasonable when the BI is not positive *)
          eapply tac_specialize_persistent_helper with _ H _ _ _ _;
            [env_reflexivity || fail "iSpecialize:" H "not found"
            |iSpecializePat H pat; last (iExact H)
@@ -540,7 +541,7 @@ Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) :=
             let Q := match goal with |- IntoPersistent _ ?Q _ => Q end in
             fail "iSpecialize:" Q "not persistent"
            |env_cbv; apply _ ||
-            let Q := match goal with |- Affine ?Q => Q end in
+            let Q := match goal with |- TCAnd _ (Affine ?Q) => Q end in
             fail "iSpecialize:" Q "not affine"
            |env_reflexivity
            |(* goal *)]
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index d2b31fd4c7d7d2333b3f3b8b0154089c7672be16..7aaec057ba3dd55f4867dca5d47efd83386c026e 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -44,9 +44,9 @@ Lemma test_unfold_constants : bar.
 Proof. iIntros (P) "HP //". Qed.
 
 Lemma test_iRewrite {A : ofeT} (x y : A) P :
-  (∀ z, P -∗ ■ (z ≡ y)) -∗ (P -∗ P ∧ (x,x) ≡ (y,x)).
+  ⬕ (∀ z, P -∗ ■ (z ≡ y)) -∗ (P -∗ P ∧ (x,x) ≡ (y,x)).
 Proof.
-  iIntros "H1 H2".
+  iIntros "#H1 H2".
   iRewrite (bi.internal_eq_sym x x with "[# //]").
   iRewrite -("H1" $! _ with "[- //]").
   auto.