diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index 574d86810fa384b21705801b2c2f39f9fa7dfd9d..68f6ffafcc7e4e352255da39eeca5daf7f7364e4 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -17,7 +17,7 @@ Implicit Types P Q : PROP.
 Lemma tac_start P : envs_entails (Envs Enil Enil 1) P → ⊢ P.
 Proof.
   rewrite envs_entails_unseal !of_envs_eq /=.
-  rewrite intuitionistically_True_emp left_id=><-.
+  rewrite left_id=><-.
   apply and_intro=> //. apply pure_intro; repeat constructor.
 Qed.
 
@@ -29,10 +29,13 @@ Lemma tac_stop Δ P :
    end ⊢ P) →
   envs_entails Δ P.
 Proof.
-  rewrite envs_entails_unseal !of_envs_eq. intros <-.
-  rewrite and_elim_r -env_to_prop_and_sound -env_to_prop_sound.
-  destruct (env_intuitionistic Δ), (env_spatial Δ);
-    by rewrite /= ?intuitionistically_True_emp ?left_id ?right_id.
+  rewrite envs_entails_unseal !of_envs_eq. intros <-. rewrite and_elim_r.
+  destruct (env_intuitionistic Δ).
+  { rewrite env_to_prop_sound and_elim_r //. }
+  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 //.
 Qed.
 
 (** * Basic rules *)
@@ -652,7 +655,8 @@ Lemma tac_and_destruct Δ i p j1 j2 P P1 P2 Q :
 Proof.
   destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
   rewrite envs_entails_unseal. intros. rewrite envs_simple_replace_sound //=. destruct p.
-  - by rewrite (into_and _ P) /= right_id -(comm _ P1) wand_elim_r.
+  - rewrite (into_and _ P) /= right_id (comm _ P1).
+    rewrite -persistently_and wand_elim_r //.
   - by rewrite /= (into_sep P) right_id -(comm _ P1) wand_elim_r.
 Qed.
 
@@ -812,7 +816,7 @@ Lemma tac_accu Δ P :
   envs_entails Δ P.
 Proof.
   rewrite envs_entails_unseal=><-.
-  rewrite env_to_prop_sound !of_envs_eq and_elim_r sep_elim_r //.
+  rewrite env_to_prop_sound !of_envs_eq and_elim_r and_elim_r //.
 Qed.
 
 (** * Invariants *)
@@ -918,7 +922,7 @@ Class TransformIntuitionisticEnv {PROP1 PROP2} (M : modality PROP1 PROP2)
   transform_intuitionistic_env :
     (∀ P Q, C P Q → □ P ⊢ M (□ Q)) →
     (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q)) →
-    □ ([∧] Γin) ⊢ M (□ ([∧] Γout));
+    <affine> ([∧] env_map_pers Γin) ⊢ M (<affine> ([∧] env_map_pers Γout));
   transform_intuitionistic_env_wf : env_wf Γin → env_wf Γout;
   transform_intuitionistic_env_dom i : Γin !! i = None → Γout !! i = None;
 }.
@@ -1015,7 +1019,7 @@ Section tac_modal_intro.
   Global Instance transform_intuitionistic_env_nil C : TransformIntuitionisticEnv M C Enil Enil.
   Proof.
     split; [|eauto using Enil_wf|done]=> /= ??.
-    rewrite !intuitionistically_True_emp -modality_emp //.
+    rewrite !affinely_True_emp -modality_emp //.
   Qed.
   Global Instance transform_intuitionistic_env_snoc (C : PROP2 → PROP1 → Prop) Γ Γ' i P Q :
     C P Q →
@@ -1023,8 +1027,11 @@ Section tac_modal_intro.
     TransformIntuitionisticEnv M C (Esnoc Γ i P) (Esnoc Γ' i Q).
   Proof.
     intros ? [HΓ Hwf Hdom]; split; simpl.
-    - intros HC Hand. rewrite intuitionistically_and HC // HΓ //.
-      by rewrite Hand -intuitionistically_and.
+    - intros HC Hand. rewrite -Hand. apply and_intro.
+      + rewrite -modality_emp affinely_elim_emp. done.
+      + rewrite affinely_and HΓ //.
+        rewrite /bi_intuitionistically in HC. rewrite HC //.
+        rewrite !affinely_elim. eauto.
     - inversion 1; constructor; auto.
     - intros j. destruct (ident_beq _ _); naive_solver.
   Qed.
@@ -1090,34 +1097,32 @@ Section tac_modal_intro.
         assert (∀ i, Γs !! i = None → Γs' !! i = None).
         { destruct HΓs as [| |?????? []| |]; eauto. }
         naive_solver. }
-    assert (□ [∧] Γp ⊢ M (□ [∧] Γp'))%I as HMp.
-    { remember (modality_intuitionistic_action M).
+    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 -modality_sep absorbingly_if_sep. f_equiv.
+    - rewrite -absorbingly_if_intro.
+      remember (modality_intuitionistic_action M).
       destruct HΓp as [? M|M C Γp ?%TCForall_Forall|? M C Γp Γp' []|? M Γp|M Γp]; simpl.
-      - rewrite {1}intuitionistically_elim_emp (modality_emp M)
-          intuitionistically_True_emp //.
-      - eauto using modality_intuitionistic_forall_big_and.
-      - eauto using modality_intuitionistic_transform,
+      + rewrite !affinely_True_emp. apply modality_emp.
+      + eauto using modality_intuitionistic_forall_big_and.
+      + eauto using modality_intuitionistic_transform,
           modality_and_transform.
-      - by rewrite {1}intuitionistically_elim_emp (modality_emp M)
-          intuitionistically_True_emp.
-      - eauto using modality_intuitionistic_id. }
-    move: HQ'; rewrite -HQ pure_True // left_id HMp=> HQ' {HQ Hwf HMp}.
-    remember (modality_spatial_action M).
-    destruct HΓs as [? M|M C Γs ?%TCForall_Forall|? M C Γs Γs' fi []|? M Γs|M Γs]; simpl.
-    - by rewrite -HQ' //= !right_id.
-    - rewrite -HQ' // {1}(modality_spatial_forall_big_sep _ _ Γs) //.
-      by rewrite modality_sep.
-    - destruct fi.
-      + rewrite -(absorbing Q') /bi_absorbingly -HQ' // (comm _ True%I).
-        rewrite -modality_sep -assoc. apply sep_mono_r.
-        eauto using modality_spatial_transform.
-      + rewrite -HQ' // -modality_sep. apply sep_mono_r.
-        rewrite -(right_id emp%I bi_sep (M _)).
-        eauto using modality_spatial_transform.
-    - rewrite -HQ' //= right_id comm -{2}(modality_spatial_clear M) //.
-      by rewrite (True_intro ([∗] Γs)).
-    - rewrite -HQ' // {1}(modality_spatial_id M ([∗] Γs)) //.
-      by rewrite -modality_sep.
+      + by rewrite {1}affinely_elim_emp affinely_True_emp (modality_emp M).
+      + eauto using modality_intuitionistic_id_big_and.
+    - remember (modality_spatial_action M).
+      destruct HΓs as [? M|M C Γs ?%TCForall_Forall|? M C Γs Γs' fi []|? M Γs|M Γs]; simpl.
+      + by rewrite modality_emp.
+      + rewrite {1}(modality_spatial_forall_big_sep _ _ Γs) //.
+      + destruct fi.
+        * rewrite /= /bi_absorbingly (comm _ True%I).
+          eauto using modality_spatial_transform.
+        * rewrite /= -(right_id emp%I bi_sep (M _)).
+          eauto using modality_spatial_transform.
+      + rewrite -{1}(modality_spatial_clear M) // -modality_emp.
+        rewrite absorbingly_emp_True. apply True_intro.
+      + rewrite {1}(modality_spatial_id M ([∗] Γs)) //.
   Qed.
 End tac_modal_intro.
 
@@ -1141,7 +1146,9 @@ Proof. by split. Qed.
 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 /= !laterN_and !laterN_sep.
+  intros [[Hp ??] [Hs ??]]; rewrite !of_envs_eq.
+  rewrite ![([∧] _ ∧ _)%I]persistent_and_affinely_sep_l.
+  rewrite !laterN_and !laterN_sep.
   rewrite -{1}laterN_intro. apply and_mono, sep_mono.
   - apply pure_mono; destruct 1; constructor; naive_solver.
   - apply Hp; rewrite /= /MaybeIntoLaterN.
diff --git a/iris/proofmode/environments.v b/iris/proofmode/environments.v
index 126286e4a974b82771a941db324c74791015e5ff..9415109158145316c46cd640bae50a34cb82f304 100644
--- a/iris/proofmode/environments.v
+++ b/iris/proofmode/environments.v
@@ -78,6 +78,12 @@ Inductive env_Forall2 {A B} (P : A → B → Prop) : env A → env B → Prop :=
   | env_Forall2_snoc Γ1 Γ2 i x y :
      env_Forall2 P Γ1 Γ2 → P x y → env_Forall2 P (Esnoc Γ1 i x) (Esnoc Γ2 i y).
 
+Fixpoint env_map {A B} (f : A → B) (Γ : env A) : env B :=
+  match Γ with
+  | Enil => Enil
+  | Esnoc Γ j x => Esnoc (env_map f Γ) j (f x)
+  end.
+
 Inductive env_subenv {A} : relation (env A) :=
   | env_subenv_nil : env_subenv Enil Enil
   | env_subenv_snoc Γ1 Γ2 i x :
@@ -193,6 +199,10 @@ Proof. intros Γ1 Γ2 HΓ i ? <-; by constructor. Qed.
 Global Instance env_to_list_proper (P : relation A) :
   Proper (env_Forall2 P ==> Forall2 P) env_to_list.
 Proof. induction 1; constructor; auto. Qed.
+Global Instance env_map_proper {B} (P : relation A) (Q : relation B) (f : A → B) :
+  Proper (P ==> Q) f →
+  Proper (env_Forall2 P ==> env_Forall2 Q) (env_map f).
+Proof. intros Hf. induction 1; constructor; auto. Qed.
 
 Lemma env_Forall2_fresh {B} (P : A → B → Prop) Γ Σ i :
   env_Forall2 P Γ Σ → Γ !! i = None → Σ !! i = None.
@@ -208,6 +218,40 @@ Proof. induction 1; inversion_clear 1; eauto using env_subenv_fresh. Qed.
 Global Instance env_to_list_subenv_proper :
   Proper (env_subenv ==> sublist) (@env_to_list A).
 Proof. induction 1; simpl; constructor; auto. Qed.
+
+Lemma env_map_lookup {B} (f : A → B) Γ i :
+  env_map f Γ !! i = f <$> Γ !! i.
+Proof.
+  induction Γ; simpl; first done.
+  case_match; naive_solver.
+Qed.
+Lemma env_map_delete {B} (f : A → B) Γ i :
+  env_map f (env_delete i Γ) = env_delete i (env_map f Γ).
+Proof.
+  induction Γ as [|? IH]; simpl; first done.
+  case_match; first naive_solver.
+  simpl. rewrite IH. done.
+Qed.
+Lemma env_map_app {B} (f : A → B) Γ1 Γ2 :
+  env_app (env_map f Γ1) (env_map f Γ2) = (env_map f) <$> env_app Γ1 Γ2.
+Proof.
+  induction Γ1 as [|Γ1 IH i]; simpl; first done.
+  rewrite IH. clear IH.
+  destruct (env_app Γ1 Γ2) as [Γ'|]; simpl; last done.
+  rewrite env_map_lookup.
+  destruct (Γ' !! i) as [x|]; done.
+Qed.
+Lemma env_map_replace {B} (f : A → B) i Γi Γ :
+  env_replace i (env_map f Γi) (env_map f Γ) = (env_map f) <$> env_replace i Γi Γ.
+Proof.
+  induction Γ as [|Γ IH j]; simpl; first done.
+  case_match.
+  { rewrite env_map_app //. }
+  rewrite IH. clear IH.
+  rewrite env_map_lookup.
+  destruct (Γi !! _) as [x|]; simpl; first done.
+  destruct (env_replace i Γi Γ) as [Γ'|]; done.
+Qed.
 End env.
 
 Record envs (PROP : bi) := Envs {
@@ -221,6 +265,14 @@ Global Arguments env_intuitionistic {_} _.
 Global Arguments env_spatial {_} _.
 Global Arguments env_counter {_} _.
 
+Notation env_map_pers Γ := (env_map bi_persistently Γ).
+Global Instance env_persistently_persistent {PROP : bi} (Γ : env PROP) :
+  Persistent ([∧] env_map_pers Γ).
+Proof. induction Γ; simpl; apply _. Qed.
+Global Instance env_persistently_absorbing {PROP : bi} (Γ : env PROP) :
+  Absorbing ([∧] env_map_pers Γ).
+Proof. induction Γ; simpl; apply _. Qed.
+
 (** We now define the judgment [envs_entails Δ Q] for proof mode entailments.
 This judgment expresses that [Q] can be proved under the proof mode environment
 [Δ]. To improve performance and to encapsulate the internals of the proof mode
@@ -249,7 +301,7 @@ Definition envs_wf {PROP : bi} (Δ : envs PROP) :=
   envs_wf' (env_intuitionistic Δ) (env_spatial Δ).
 
 Definition of_envs' {PROP : bi} (Γp Γs : env PROP) : PROP :=
-  (⌜envs_wf' Γp Γs⌝ ∧ □ [∧] Γp ∗ [∗] Γs)%I.
+  (⌜envs_wf' Γp Γs⌝ ∧ [∧] (env_map_pers Γp) ∧ [∗] Γs)%I.
 Global Instance: Params (@of_envs') 1 := {}.
 Definition of_envs {PROP : bi} (Δ : envs PROP) : PROP :=
   of_envs' (env_intuitionistic Δ) (env_spatial Δ).
@@ -384,13 +436,19 @@ Implicit Types Δ : envs PROP.
 Implicit Types P Q : PROP.
 
 Lemma of_envs_eq Δ :
-  of_envs Δ = (⌜envs_wf Δ⌝ ∧ □ [∧] env_intuitionistic Δ ∗ [∗] env_spatial Δ)%I.
+  of_envs Δ =
+  (⌜envs_wf Δ⌝ ∧
+    [∧] (env_map_pers (env_intuitionistic Δ)) ∧
+    [∗] env_spatial Δ)%I.
 Proof. done. Qed.
 (** An environment is a ∗ of something intuitionistic and the spatial environment.
 TODO: Can we define it as such? *)
 Lemma of_envs_eq' Δ :
-  of_envs Δ ⊣⊢ (⌜envs_wf Δ⌝ ∧ □ [∧] env_intuitionistic Δ) ∗ [∗] env_spatial Δ.
-Proof. rewrite of_envs_eq persistent_and_sep_assoc //. Qed.
+  of_envs Δ ⊣⊢
+  (⌜envs_wf Δ⌝ ∧ <affine> [∧] (env_map_pers (env_intuitionistic Δ))) ∗ [∗] env_spatial Δ.
+Proof.
+  rewrite of_envs_eq [([∧] _ ∧ _)%I]persistent_and_affinely_sep_l persistent_and_sep_assoc //.
+Qed.
 
 Global Instance envs_Forall2_refl (R : relation PROP) :
   Reflexive R → Reflexive (envs_Forall2 R).
@@ -483,18 +541,25 @@ Lemma envs_lookup_sound' Δ rp i p P :
 Proof.
   rewrite /envs_lookup /envs_delete !of_envs_eq=>?.
   apply pure_elim_l=> Hwf.
-  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
+  destruct Δ as [Γp Γs], (Γp !! i) eqn:Heqo; simplify_eq/=.
   - rewrite pure_True ?left_id; last (destruct Hwf, rp; constructor;
       naive_solver eauto using env_delete_wf, env_delete_fresh).
-    destruct rp.
-    + rewrite (env_lookup_perm Γp) //= intuitionistically_and.
-      by rewrite and_sep_intuitionistically -assoc.
-    + rewrite {1}intuitionistically_sep_dup {1}(env_lookup_perm Γp) //=.
-      by rewrite intuitionistically_and and_elim_l -assoc.
+    rewrite -persistently_and_intuitionistically_sep_l assoc.
+    apply and_mono; last done. apply and_intro.
+    + rewrite (env_lookup_perm (env_map_pers Γp)).
+      2:{ rewrite env_map_lookup. erewrite Heqo. done. }
+      simpl. rewrite and_elim_l. done.
+    + destruct rp; last done.
+      rewrite (env_lookup_perm (env_map_pers Γp)).
+      2:{ rewrite env_map_lookup. erewrite Heqo. done. }
+      simpl. rewrite and_elim_r. rewrite env_map_delete //.
   - 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).
-    rewrite (env_lookup_perm Γs) //=. by rewrite !assoc -(comm _ P).
+    rewrite (env_lookup_perm Γs) //=.
+    rewrite ![(P ∗ _)%I]comm.
+    rewrite persistent_and_sep_assoc.
+    done.
 Qed.
 Lemma envs_lookup_sound Δ i p P :
   envs_lookup i Δ = Some (p,P) →
@@ -509,11 +574,18 @@ Lemma envs_lookup_sound_2 Δ i p P :
 Proof.
   rewrite /envs_lookup !of_envs_eq=>Hwf ?.
   rewrite [⌜envs_wf Δ⌝%I]pure_True // left_id.
-  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
-  - by rewrite (env_lookup_perm Γp) //= intuitionistically_and
-      and_sep_intuitionistically and_elim_r assoc.
+  destruct Δ as [Γp Γs], (Γp !! i) eqn:Heqo; simplify_eq/=.
+  - rewrite -persistently_and_intuitionistically_sep_l.
+    rewrite (env_lookup_perm (env_map_pers Γp)).
+    2:{ rewrite env_map_lookup. erewrite Heqo. done. }
+    rewrite !assoc. apply and_mono; last done. simpl.
+    rewrite -!assoc. apply and_mono; first done.
+    rewrite and_elim_r. rewrite env_map_delete. done.
   - destruct (Γs !! i) eqn:?; simplify_eq/=.
-    by rewrite (env_lookup_perm Γs) //= and_elim_r !assoc (comm _ P).
+    rewrite (env_lookup_perm Γs) //=.
+    rewrite [(⌜_⌝ ∧ _)%I]and_elim_r.
+    rewrite (comm _ P) -persistent_and_sep_assoc.
+    apply and_mono; first done. rewrite comm //.
 Qed.
 
 Lemma envs_lookup_split Δ i p P :
@@ -575,35 +647,40 @@ 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.
-    + by rewrite intuitionistically_and and_sep_intuitionistically assoc.
+    + rewrite -persistently_and_intuitionistically_sep_l assoc //.
   - apply and_intro; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
       intros j; destruct (ident_beq_reflect j i); naive_solver.
-    + by rewrite !assoc (comm _ P).
+    + rewrite (comm _ P) -persistent_and_sep_assoc.
+      apply and_mono; first done. rewrite comm //.
 Qed.
 
 Lemma envs_app_sound Δ Δ' p Γ :
   envs_app p Γ Δ = Some Δ' →
-  of_envs Δ ⊢ (if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ'.
+  of_envs Δ ⊢ (if p then <affine> [∧] (env_map_pers Γ) else [∗] Γ) -∗ of_envs Δ'.
 Proof.
   rewrite !of_envs_eq /envs_app=> ?; apply pure_elim_l=> Hwf.
   destruct Δ as [Γp Γs], p; simplify_eq/=.
   - destruct (env_app Γ Γs) eqn:Happ,
-      (env_app Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
+      (env_app Γ Γp) as [Γp'|] eqn:Heqo; simplify_eq/=.
     apply wand_intro_l, and_intro; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using env_app_wf.
       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 intuitionistically_and and_sep_intuitionistically.
-      by rewrite assoc.
+    + apply and_intro.
+      * rewrite and_elim_l. rewrite (env_app_perm _ _ (env_map_pers Γp')).
+        2:{ erewrite env_map_app. erewrite Heqo. done. }
+        rewrite affinely_elim big_opL_app sep_and. done.
+      * rewrite and_elim_r. rewrite sep_elim_r. done.
   - destruct (env_app Γ Γp) eqn:Happ,
       (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
     apply wand_intro_l, and_intro; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using env_app_wf.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       naive_solver eauto using env_app_fresh.
-    + by rewrite (env_app_perm _ _ Γs') // big_opL_app !assoc (comm _ ([∗] Γ)%I).
+    + rewrite (env_app_perm _ _ Γs') // big_opL_app. apply and_intro.
+      * rewrite and_elim_l. rewrite sep_elim_r. done.
+      * rewrite and_elim_r. done.
 Qed.
 
 Lemma envs_app_singleton_sound Δ Δ' p j Q :
@@ -612,19 +689,22 @@ 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 Δ' →
-  of_envs (envs_delete true i p Δ) ⊢ (if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ'.
+  of_envs (envs_delete true i p Δ) ⊢ (if p then <affine> [∧] (env_map_pers Γ) else [∗] Γ) -∗ of_envs Δ'.
 Proof.
   rewrite /envs_simple_replace /envs_delete !of_envs_eq=> ?.
   apply pure_elim_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
   - destruct (env_app Γ Γs) eqn:Happ,
-      (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
+      (env_replace i Γ Γp) as [Γp'|] eqn:Heqo; simplify_eq/=.
     apply wand_intro_l, and_intro; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using env_replace_wf.
       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 intuitionistically_and and_sep_intuitionistically.
-      by rewrite assoc.
+    + rewrite (env_replace_perm _ _ (env_map_pers Γp')).
+      2:{ erewrite env_map_replace. erewrite Heqo. done. }
+      rewrite big_opL_app. apply and_intro; first apply and_intro.
+      * rewrite and_elim_l affinely_elim sep_elim_l. done.
+      * rewrite sep_elim_r and_elim_l. rewrite env_map_delete. done.
+      * rewrite and_elim_r sep_elim_r. done.
   - destruct (env_app Γ Γp) eqn:Happ,
       (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
     apply wand_intro_l, and_intro; [apply pure_intro|].
@@ -632,7 +712,9 @@ 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 _ _ Γs') // big_opL_app.
-      by rewrite !assoc (comm _ ([∗] Γ)%I).
+      apply and_intro.
+      * rewrite and_elim_l. rewrite sep_elim_r. done.
+      * rewrite and_elim_r. done.
 Qed.
 
 Lemma envs_simple_replace_singleton_sound' Δ Δ' i p j Q :
@@ -642,12 +724,12 @@ Proof. move=> /envs_simple_replace_sound'. destruct p; by rewrite /= right_id. Q
 
 Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
   envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
-  of_envs Δ ⊢ □?p P ∗ ((if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ').
+  of_envs Δ ⊢ □?p P ∗ ((if p then <affine> [∧] (env_map_pers Γ) else [∗] Γ) -∗ of_envs Δ').
 Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.
 
 Lemma envs_simple_replace_maybe_sound Δ Δ' i p P Γ :
   envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
-  of_envs Δ ⊢ □?p P ∗ (((if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ') ∧ (□?p P -∗ of_envs Δ)).
+  of_envs Δ ⊢ □?p P ∗ (((if p then <affine> [∧] (env_map_pers Γ) else [∗] Γ) -∗ of_envs Δ') ∧ (□?p P -∗ of_envs Δ)).
 Proof.
   intros. apply pure_elim with (envs_wf Δ).
   { rewrite of_envs_eq. apply and_elim_l. }
@@ -666,7 +748,7 @@ Qed.
 
 Lemma envs_replace_sound' Δ Δ' i p q Γ :
   envs_replace i p q Γ Δ = Some Δ' →
-  of_envs (envs_delete true i p Δ) ⊢ (if q then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ'.
+  of_envs (envs_delete true i p Δ) ⊢ (if q then <affine> [∧] (env_map_pers Γ) else [∗] Γ) -∗ of_envs Δ'.
 Proof.
   rewrite /envs_replace; destruct (beq _ _) eqn:Hpq.
   - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
@@ -680,7 +762,7 @@ 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 Δ' →
-  of_envs Δ ⊢ □?p P ∗ ((if q then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ').
+  of_envs Δ ⊢ □?p P ∗ ((if q then <affine> [∧] (env_map_pers Γ) else [∗] Γ) -∗ of_envs Δ').
 Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.
 
 Lemma envs_replace_singleton_sound Δ Δ' i p q P j Q :
@@ -702,16 +784,18 @@ 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 right_id -persistent_and_sep_assoc. apply and_intro; [|done].
-  apply pure_intro. destruct Hwf; constructor; simpl; auto using Enil_wf.
+  rewrite -persistent_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.
 Qed.
 
 Lemma env_spatial_is_nil_intuitionistically Δ :
   env_spatial_is_nil Δ = true → of_envs Δ ⊢ □ of_envs Δ.
 Proof.
   intros. rewrite !of_envs_eq; destruct Δ as [? []]; simplify_eq/=.
-  rewrite !right_id /bi_intuitionistically {1}affinely_and_r persistently_and.
-  by rewrite persistently_affinely_elim persistently_idemp persistently_pure.
+  rewrite /bi_intuitionistically !persistently_and.
+  rewrite persistently_pure persistent_persistently -persistently_emp_2.
+  apply and_intro; last done. rewrite !and_elim_r. done.
 Qed.
 
 Lemma envs_lookup_envs_delete Δ i p P :
@@ -779,11 +863,14 @@ Proof.
   - rewrite /= IH (comm _ Q _) assoc. done.
 Qed.
 
-Lemma env_to_prop_and_sound Γ : env_to_prop_and Γ ⊣⊢ [∧] Γ.
+Lemma env_to_prop_and_pers_sound Γ :
+  □ env_to_prop_and Γ ⊣⊢ <affine> [∧] (env_map_pers Γ).
 Proof.
-  destruct Γ as [|Γ i P]; simpl; first done.
+  destruct Γ as [|Γ i P]; simpl.
+  { rewrite /bi_intuitionistically persistent_persistently //. }
   revert P. induction Γ as [|Γ IH ? Q]=>P; simpl.
   - by rewrite right_id.
-  - rewrite /= IH (comm _ Q _) assoc. done.
+  - rewrite /= IH (comm _ Q _) assoc. f_equiv.
+    rewrite persistently_and. done.
 Qed.
 End envs.
diff --git a/iris/proofmode/modalities.v b/iris/proofmode/modalities.v
index 37094e2a72d5ce6cd9d52c8a2209bf58e2b75ae0..315be368bb48a989705ccb84e30bc69f22747e40 100644
--- a/iris/proofmode/modalities.v
+++ b/iris/proofmode/modalities.v
@@ -1,5 +1,6 @@
 From stdpp Require Import namespaces.
 From iris.bi Require Export bi.
+From iris.proofmode Require Export environments.
 From iris.prelude Require Import options.
 Import bi.
 
@@ -158,14 +159,29 @@ Section modality1.
     modality_spatial_action M = MIEnvId → P ⊢ M P.
   Proof. destruct M as [??? []]; naive_solver. Qed.
 
-  Lemma modality_intuitionistic_forall_big_and C Ps :
+  Lemma modality_intuitionistic_forall_big_and C Γ :
     modality_intuitionistic_action M = MIEnvForall C →
-    Forall C Ps → □ [∧] Ps ⊢ M (□ [∧] Ps).
+    Forall C (env_to_list Γ) →
+    <affine> [∧] (env_map_pers Γ) ⊢ M (<affine> [∧] (env_map_pers Γ)).
   Proof.
-    induction 2 as [|P Ps ? _ IH]; simpl.
-    - by rewrite intuitionistically_True_emp -modality_emp.
-    - rewrite intuitionistically_and -modality_and_forall // -IH.
-      by rewrite {1}(modality_intuitionistic_forall _ P).
+    induction Γ as [|Γ IH i P]; intros ? HΓ; simpl.
+    - rewrite affinely_True_emp. apply modality_emp.
+    - inversion HΓ; subst. clear HΓ.
+      rewrite affinely_and -modality_and_forall //. apply and_mono.
+      + by eapply modality_intuitionistic_forall.
+      + eauto.
+  Qed.
+  Lemma modality_intuitionistic_id_big_and Γ :
+    modality_intuitionistic_action M = MIEnvId →
+    <affine> [∧] (env_map_pers Γ) ⊢ M (<affine> [∧] (env_map_pers Γ)).
+  Proof.
+    intros. induction Γ as [|Γ IH i P]; simpl.
+    - rewrite affinely_True_emp. apply modality_emp.
+    - rewrite affinely_and {1}IH. clear IH.
+      rewrite persistent_and_affinely_sep_l_1.
+      rewrite {1}[(<affine> <pers> P)%I]modality_intuitionistic_id //.
+      rewrite affinely_elim modality_sep. f_equiv.
+      apply: sep_and.
   Qed.
   Lemma modality_spatial_forall_big_sep C Ps :
     modality_spatial_action M = MIEnvForall C →