diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index fb8e2dbf1a37c61faa902e6d1932cd15bdffff68..a76d31eea67581f4393704676f3c86be27cc85b8 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -9,8 +9,8 @@ Section bi_modalities.
   Lemma modality_persistently_mixin :
     modality_mixin (@bi_persistently PROP) MIEnvId MIEnvClear.
   Proof.
-    split; eauto using equiv_entails_sym, persistently_intro, persistently_mono,
-      persistently_sep_2 with typeclass_instances.
+    split; simpl; eauto using equiv_entails_sym, persistently_intro,
+      persistently_mono, persistently_sep_2 with typeclass_instances.
   Qed.
   Definition modality_persistently :=
     Modality _ modality_persistently_mixin.
@@ -18,7 +18,7 @@ Section bi_modalities.
   Lemma modality_affinely_mixin :
     modality_mixin (@bi_affinely PROP) MIEnvId (MIEnvForall Affine).
   Proof.
-    split; eauto using equiv_entails_sym, affinely_intro, affinely_mono,
+    split; simpl; eauto using equiv_entails_sym, affinely_intro, affinely_mono,
       affinely_sep_2 with typeclass_instances.
   Qed.
   Definition modality_affinely :=
@@ -27,7 +27,7 @@ Section bi_modalities.
   Lemma modality_affinely_persistently_mixin :
     modality_mixin (λ P : PROP, □ P)%I MIEnvId MIEnvIsEmpty.
   Proof.
-    split; eauto using equiv_entails_sym, affinely_persistently_emp,
+    split; simpl; eauto using equiv_entails_sym, affinely_persistently_emp,
       affinely_mono, persistently_mono, affinely_persistently_idemp,
       affinely_persistently_sep_2 with typeclass_instances.
   Qed.
@@ -37,8 +37,8 @@ Section bi_modalities.
   Lemma modality_plainly_mixin :
     modality_mixin (@bi_plainly PROP) (MIEnvForall Plain) MIEnvClear.
   Proof.
-    split; split_and?; eauto using equiv_entails_sym, plainly_intro, plainly_mono,
-      plainly_and, plainly_sep_2 with typeclass_instances.
+    split; simpl; split_and?; eauto using equiv_entails_sym, plainly_intro,
+      plainly_mono, plainly_and, plainly_sep_2 with typeclass_instances.
   Qed.
   Definition modality_plainly :=
     Modality _ modality_plainly_mixin.
@@ -46,7 +46,8 @@ Section bi_modalities.
   Lemma modality_affinely_plainly_mixin :
     modality_mixin (λ P : PROP, ■ P)%I (MIEnvForall Plain) MIEnvIsEmpty.
   Proof.
-    split; split_and?; eauto using equiv_entails_sym, affinely_plainly_emp, affinely_intro,
+    split; simpl; split_and?; eauto using equiv_entails_sym,
+      affinely_plainly_emp, affinely_intro,
       plainly_intro, affinely_mono, plainly_mono, affinely_plainly_idemp,
       affinely_plainly_and, affinely_plainly_sep_2 with typeclass_instances.
   Qed.
@@ -56,7 +57,7 @@ Section bi_modalities.
   Lemma modality_absorbingly_mixin :
     modality_mixin (@bi_absorbingly PROP) MIEnvId MIEnvId.
   Proof.
-    split; eauto using equiv_entails_sym, absorbingly_intro,
+    split; simpl; eauto using equiv_entails_sym, absorbingly_intro,
       absorbingly_mono, absorbingly_sep.
   Qed.
   Definition modality_absorbingly :=
@@ -69,7 +70,7 @@ Section sbi_modalities.
   Lemma modality_except_0_mixin :
     modality_mixin (@sbi_except_0 PROP) MIEnvId MIEnvId.
   Proof.
-    split; eauto using equiv_entails_sym,
+    split; simpl; eauto using equiv_entails_sym,
       except_0_intro, except_0_mono, except_0_sep.
   Qed.
   Definition modality_except_0 :=
@@ -79,8 +80,8 @@ Section sbi_modalities.
     modality_mixin (@sbi_laterN PROP n)
       (MIEnvTransform (MaybeIntoLaterN false n)) (MIEnvTransform (MaybeIntoLaterN false n)).
   Proof.
-    split; split_and?; eauto using equiv_entails_sym, laterN_intro, laterN_mono,
-      laterN_and, laterN_sep with typeclass_instances.
+    split; simpl; split_and?; eauto using equiv_entails_sym, laterN_intro,
+      laterN_mono, laterN_and, laterN_sep with typeclass_instances.
     rewrite /MaybeIntoLaterN=> P Q ->. by rewrite laterN_affinely_persistently_2.
   Qed.
   Definition modality_laterN n :=
@@ -88,13 +89,13 @@ Section sbi_modalities.
 
   Lemma modality_bupd_mixin `{BUpdFacts PROP} :
     modality_mixin (@bupd PROP _) MIEnvId MIEnvId.
-  Proof. split; eauto using bupd_intro, bupd_mono, bupd_sep. Qed.
+  Proof. split; simpl; eauto using bupd_intro, bupd_mono, bupd_sep. Qed.
   Definition modality_bupd `{BUpdFacts PROP} :=
     Modality _ modality_bupd_mixin.
 
   Lemma modality_fupd_mixin `{FUpdFacts PROP} E :
     modality_mixin (@fupd PROP _ E E) MIEnvId MIEnvId.
-  Proof. split; eauto using fupd_intro, fupd_mono, fupd_sep. Qed.
+  Proof. split; simpl; eauto using fupd_intro, fupd_mono, fupd_sep. Qed.
   Definition modality_fupd `{FUpdFacts PROP} E :=
     Modality _ (modality_fupd_mixin E).
 End sbi_modalities.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 1443eb7cf81d7535745565e8ab3d8fa922565f58..391cd720f4f29243f9502bc36b6d5ecae69d0d23 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -101,86 +101,81 @@ spatial what action should be performed upon introducing the modality:
 
 Formally, these actions correspond to the following inductive type: *)
 
-Inductive modality_intro_spec (PROP : bi) :=
-  | MIEnvIsEmpty
-  | MIEnvForall (C : PROP → Prop)
-  | MIEnvTransform (C : PROP → PROP → Prop)
-  | MIEnvClear
-  | MIEnvId.
-Arguments MIEnvIsEmpty {_}.
+Inductive modality_intro_spec (PROP1 : bi) : bi → Type :=
+  | MIEnvIsEmpty {PROP2 : bi} : modality_intro_spec PROP1 PROP2
+  | MIEnvForall (C : PROP1 → Prop) : modality_intro_spec PROP1 PROP1
+  | MIEnvTransform {PROP2 : bi} (C : PROP2 → PROP1 → Prop) : modality_intro_spec PROP1 PROP2
+  | MIEnvClear {PROP2} : modality_intro_spec PROP1 PROP2
+  | MIEnvId : modality_intro_spec PROP1 PROP1.
+Arguments MIEnvIsEmpty {_ _}.
 Arguments MIEnvForall {_} _.
-Arguments MIEnvTransform {_} _.
-Arguments MIEnvClear {_}.
+Arguments MIEnvTransform {_ _} _.
+Arguments MIEnvClear {_ _}.
 Arguments MIEnvId {_}.
 
 Notation MIEnvFilter C := (MIEnvTransform (TCDiag C)).
 
+Definition modality_intro_spec_persistent {PROP1 PROP2}
+    (s : modality_intro_spec PROP1 PROP2) : (PROP1 → PROP2) → Prop :=
+  match s with
+  | MIEnvIsEmpty => λ M, True
+  | MIEnvForall C => λ M,
+     (∀ P, C P → □ P ⊢ M (□ P)) ∧
+     (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q))
+  | MIEnvTransform C => λ M,
+     (∀ P Q, C P Q → □ P ⊢ M (□ Q)) ∧
+     (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q))
+  | MIEnvClear => λ M, True
+  | MIEnvId => λ M, ∀ P, □ P ⊢ M (□ P)
+  end.
+
+Definition modality_intro_spec_spatial {PROP1 PROP2}
+    (s : modality_intro_spec PROP1 PROP2) : (PROP1 → PROP2) → Prop :=
+  match s with
+  | MIEnvIsEmpty => λ M, True
+  | MIEnvForall C => λ M, ∀ P, C P → P ⊢ M P
+  | MIEnvTransform C => λ M, ∀ P Q, C P Q → P ⊢ M Q
+  | MIEnvClear => λ M, ∀ P, Absorbing (M P)
+  | MIEnvId => λ M, ∀ P, P ⊢ M P
+  end.
+
 (* A modality is then a record packing together the modality with the laws it
 should satisfy to justify the given actions for both contexts: *)
-Record modality_mixin {PROP : bi} (M : PROP → PROP)
-    (pspec sspec : modality_intro_spec PROP) := {
-  modality_mixin_persistent :
-    match pspec with
-    | MIEnvIsEmpty => True
-    | MIEnvForall C => (∀ P, C P → □ P ⊢ M (□ P)) ∧ (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q))
-    | MIEnvTransform C => (∀ P Q, C P Q → □ P ⊢ M (□ Q)) ∧ (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q))
-    | MIEnvClear => True
-    | MIEnvId => ∀ P, □ P ⊢ M (□ P)
-    end;
-  modality_mixin_spatial :
-    match sspec with
-    | MIEnvIsEmpty => True
-    | MIEnvForall C => ∀ P, C P → P ⊢ M P
-    | MIEnvTransform C => (∀ P Q, C P Q → P ⊢ M Q)
-    | MIEnvClear => ∀ P, Absorbing (M P)
-    | MIEnvId => ∀ P, P ⊢ M P
-    end;
+Record modality_mixin {PROP1 PROP2 : bi} (M : PROP1 → PROP2)
+    (pspec sspec : modality_intro_spec PROP1 PROP2) := {
+  modality_mixin_persistent : modality_intro_spec_persistent pspec M;
+  modality_mixin_spatial : modality_intro_spec_spatial sspec M;
   modality_mixin_emp : emp ⊢ M emp;
   modality_mixin_mono P Q : (P ⊢ Q) → M P ⊢ M Q;
   modality_mixin_sep P Q : M P ∗ M Q ⊢ M (P ∗ Q)
 }.
 
-Record modality (PROP : bi) := Modality {
-  modality_car :> PROP → PROP;
-  modality_persistent_spec : modality_intro_spec PROP;
-  modality_spatial_spec : modality_intro_spec PROP;
+Record modality (PROP1 PROP2 : bi) := Modality {
+  modality_car :> PROP1 → PROP2;
+  modality_persistent_spec : modality_intro_spec PROP1 PROP2;
+  modality_spatial_spec : modality_intro_spec PROP1 PROP2;
   modality_mixin_of :
     modality_mixin modality_car modality_persistent_spec modality_spatial_spec
 }.
-Arguments Modality {_} _ {_ _} _.
-Arguments modality_persistent_spec {_} _.
-Arguments modality_spatial_spec {_} _.
+Arguments Modality {_ _} _ {_ _} _.
+Arguments modality_persistent_spec {_ _} _.
+Arguments modality_spatial_spec {_ _} _.
 
 Section modality.
-  Context {PROP} (M : modality PROP).
+  Context {PROP1 PROP2} (M : modality PROP1 PROP2).
 
-  Lemma modality_persistent_forall C P :
-    modality_persistent_spec M = MIEnvForall C → C P → □ P ⊢ M (□ P).
-  Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma modality_and_forall C P Q :
-    modality_persistent_spec M = MIEnvForall C → M P ∧ M Q ⊢ M (P ∧ Q).
-  Proof. destruct M as [??? []]; naive_solver. Qed.
   Lemma modality_persistent_transform C P Q :
     modality_persistent_spec M = MIEnvTransform C → C P Q → □ P ⊢ M (□ Q).
   Proof. destruct M as [??? []]; naive_solver. Qed.
   Lemma modality_and_transform C P Q :
     modality_persistent_spec M = MIEnvTransform C → M P ∧ M Q ⊢ M (P ∧ Q).
   Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma modality_persistent_id P :
-    modality_persistent_spec M = MIEnvId → □ P ⊢ M (□ P).
-  Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma modality_spatial_forall C P :
-    modality_spatial_spec M = MIEnvForall C → C P → P ⊢ M P.
-  Proof. destruct M as [??? []]; naive_solver. Qed.
   Lemma modality_spatial_transform C P Q :
     modality_spatial_spec M = MIEnvTransform C → C P Q → P ⊢ M Q.
   Proof. destruct M as [??? []]; naive_solver. Qed.
   Lemma modality_spatial_clear P :
     modality_spatial_spec M = MIEnvClear → Absorbing (M P).
   Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma modality_spatial_id P :
-    modality_spatial_spec M = MIEnvId → P ⊢ M P.
-  Proof. destruct M as [??? []]; naive_solver. Qed.
 
   Lemma modality_emp : emp ⊢ M emp.
   Proof. eapply modality_mixin_emp, modality_mixin_of. Qed.
@@ -194,6 +189,26 @@ Section modality.
   Proof. intros P Q. apply modality_mono. Qed.
   Global Instance modality_proper : Proper ((≡) ==> (≡)) M.
   Proof. intros P Q. rewrite !equiv_spec=> -[??]; eauto using modality_mono. Qed.
+End modality.
+
+Section modality1.
+  Context {PROP} (M : modality PROP PROP).
+
+  Lemma modality_persistent_forall C P :
+    modality_persistent_spec M = MIEnvForall C → C P → □ P ⊢ M (□ P).
+  Proof. destruct M as [??? []]; naive_solver. Qed.
+  Lemma modality_and_forall C P Q :
+    modality_persistent_spec M = MIEnvForall C → M P ∧ M Q ⊢ M (P ∧ Q).
+  Proof. destruct M as [??? []]; naive_solver. Qed.
+  Lemma modality_persistent_id P :
+    modality_persistent_spec M = MIEnvId → □ P ⊢ M (□ P).
+  Proof. destruct M as [??? []]; naive_solver. Qed.
+  Lemma modality_spatial_forall C P :
+    modality_spatial_spec M = MIEnvForall C → C P → P ⊢ M P.
+  Proof. destruct M as [??? []]; naive_solver. Qed.
+  Lemma modality_spatial_id P :
+    modality_spatial_spec M = MIEnvId → P ⊢ M P.
+  Proof. destruct M as [??? []]; naive_solver. Qed.
 
   Lemma modality_persistent_forall_big_and C Ps :
     modality_persistent_spec M = MIEnvForall C →
@@ -212,13 +227,14 @@ Section modality.
     - by rewrite -modality_emp.
     - by rewrite -modality_sep -IH {1}(modality_spatial_forall _ P).
   Qed.
-End modality.
+End modality1.
 
-Class FromModal {PROP : bi} (M : modality PROP) (P Q : PROP) :=
+Class FromModal {PROP1 PROP2 : bi}
+    (M : modality PROP1 PROP2) (P : PROP2) (Q : PROP1) :=
   from_modal : M Q ⊢ P.
-Arguments FromModal {_} _ _%I _%I : simpl never.
-Arguments from_modal {_} _ _%I _%I {_}.
-Hint Mode FromModal + - ! - : typeclass_instances.
+Arguments FromModal {_ _} _ _%I _%I : simpl never.
+Arguments from_modal {_ _} _ _%I _%I {_}.
+Hint Mode FromModal - + - ! - : typeclass_instances.
 
 Class FromAffinely {PROP : bi} (P Q : PROP) :=
   from_affinely : bi_affinely Q ⊢ P.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index ef83f30cc5c78147234791ba5c815252ce2aba23..992bf1a2d5424852faf2cb16a01ebd0147e56e55 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -1036,148 +1036,6 @@ Proof.
 Qed.
 
 (** * Modalities *)
-(** Transforming *)
-Class TransformPersistentEnv
-    (M : modality PROP) (C : PROP → PROP → Prop) (Γ1 Γ2 : env PROP) := {
-  transform_persistent_env :
-    (∀ P Q, C P Q → □ P ⊢ M (□ Q)) →
-    (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q)) →
-    □ ([∧] Γ1) ⊢ M (□ ([∧] Γ2));
-  transform_persistent_env_wf : env_wf Γ1 → env_wf Γ2;
-  transform_persistent_env_dom i : Γ1 !! i = None → Γ2 !! i = None;
-}.
-Global Instance transform_persistent_env_nil M C : TransformPersistentEnv M C Enil Enil.
-Proof.
-  split=> // HC /=. rewrite !persistently_pure !affinely_True_emp.
-  by rewrite affinely_emp -modality_emp.
-Qed.
-Global Instance transform_persistent_env_snoc M (C : PROP → PROP → Prop) Γ Γ' i P Q :
-  C P Q →
-  TransformPersistentEnv M C Γ Γ' →
-  TransformPersistentEnv M C (Esnoc Γ i P) (Esnoc Γ' i Q).
-Proof.
-  intros ? [HΓ Hwf Hdom]; split; simpl.
-  - intros HC Hand. rewrite affinely_persistently_and HC // HΓ //.
-    by rewrite Hand -affinely_persistently_and.
-  - inversion 1; constructor; auto.
-  - intros j. destruct (ident_beq _ _); naive_solver.
-Qed.
-Global Instance transform_persistent_env_snoc_not M (C : PROP → PROP → Prop) Γ Γ' i P :
-  TransformPersistentEnv M C Γ Γ' →
-  TransformPersistentEnv M C (Esnoc Γ i P) Γ' | 100.
-Proof.
-  intros [HΓ Hwf Hdom]; split; simpl.
-  - intros HC Hand. by rewrite and_elim_r HΓ.
-  - inversion 1; auto.
-  - intros j. destruct (ident_beq _ _); naive_solver.
-Qed.
-
-Class TransformSpatialEnv
-    (M : modality PROP) (C : PROP → PROP → Prop)
-    (Γ1 Γ2 : env PROP) (filtered : bool) := {
-  transform_spatial_env :
-    (∀ P Q, C P Q → P ⊢ M Q) →
-    ([∗] Γ1) ⊢ M ([∗] Γ2) ∗ if filtered then True else emp;
-  transform_spatial_env_wf : env_wf Γ1 → env_wf Γ2;
-  transform_spatial_env_dom i : Γ1 !! i = None → Γ2 !! i = None;
-}.
-Global Instance transform_spatial_env_nil M C :
-  TransformSpatialEnv M C Enil Enil false.
-Proof. split=> // HC /=. by rewrite right_id -modality_emp. Qed.
-Global Instance transform_spatial_env_snoc M (C : PROP → PROP → Prop) Γ Γ' i P Q fi :
-  C P Q →
-  TransformSpatialEnv M C Γ Γ' fi →
-  TransformSpatialEnv M C (Esnoc Γ i P) (Esnoc Γ' i Q) fi.
-Proof.
-  intros ? [HΓ Hwf Hdom]; split; simpl.
-  - intros HC. by rewrite {1}(HC P) // HΓ // assoc modality_sep.
-  - inversion 1; constructor; auto.
-  - intros j. destruct (ident_beq _ _); naive_solver.
-Qed.
-
-Global Instance transform_spatial_env_snoc_not
-    M (C : PROP → PROP → Prop) Γ Γ' i P fi fi' :
-  TransformSpatialEnv M C Γ Γ' fi →
-  TCIf (TCEq fi false)
-    (TCIf (Affine P) (TCEq fi' false) (TCEq fi' true))
-    (TCEq fi' true) →
-  TransformSpatialEnv M C (Esnoc Γ i P) Γ' fi' | 100.
-Proof.
-  intros [HΓ Hwf Hdom] Hif; split; simpl.
-  - intros ?. rewrite HΓ //. destruct Hif as [-> [? ->| ->]| ->].
-    + by rewrite (affine P) left_id.
-    + by rewrite right_id comm (True_intro P).
-    + by rewrite comm -assoc (True_intro (_ ∗ P)%I).
-  - inversion 1; auto.
-  - intros j. destruct (ident_beq _ _); naive_solver.
-Qed.
-
-(** The actual introduction tactic *)
-Ltac tac_modal_cases fi :=
-  simplify_eq/=;
-  repeat match goal with
-  | H : TCAnd _ _ |- _ => destruct H
-  | H : TCEq ?x _ |- _ => inversion H; subst x; clear H
-  | H : TCForall _ _ |- _ => apply TCForall_Forall in H
-  | H : TransformPersistentEnv _ _ _ _ |- _ => destruct H
-  | H : ∃ fi, TransformSpatialEnv _ _ _ _ fi ∧ _ |- _ => destruct H as [fi [[] ?]]
-  end; simpl; auto using Enil_wf.
-
-Lemma tac_modal_intro Γp Γs Γp' Γs' M Q Q' :
-  FromModal M Q' Q →
-  match modality_persistent_spec M with
-  | MIEnvForall C => TCAnd (TCForall C (env_to_list Γp)) (TCEq Γp Γp')
-  | MIEnvTransform C => TransformPersistentEnv M C Γp Γp'
-  | MIEnvIsEmpty => TCAnd (TCEq Γp Enil) (TCEq Γp' Enil)
-  | MIEnvClear => TCEq Γp' Enil
-  | MIEnvId => TCEq Γp Γp'
-  end →
-  match modality_spatial_spec M with
-  | MIEnvForall C => TCAnd (TCForall C (env_to_list Γs)) (TCEq Γs Γs')
-  | MIEnvTransform C =>
-     ∃ fi, TransformSpatialEnv M C Γs Γs' fi ∧
-     if fi then Absorbing Q' else TCTrue
-  | MIEnvIsEmpty => TCAnd (TCEq Γs Enil) (TCEq Γs' Enil)
-  | MIEnvClear => TCEq Γs' Enil
-  | MIEnvId => TCEq Γs Γs'
-  end →
-  envs_entails (Envs Γp' Γs') Q → envs_entails (Envs Γp Γs) Q'.
-Proof.
-  rewrite envs_entails_eq /FromModal /of_envs /= => HQ' HΓp HΓs HQ.
-  apply pure_elim_l=> -[???]. assert (envs_wf (Envs Γp' Γs')) as Hwf.
-  { split; simpl in *.
-    - destruct (modality_persistent_spec M); tac_modal_cases fi.
-    - destruct (modality_spatial_spec M); tac_modal_cases fi.
-    - destruct (modality_persistent_spec M),
-        (modality_spatial_spec M); tac_modal_cases fi; naive_solver. }
-  assert (□ [∧] Γp ⊢ M (□ [∧] Γp'))%I as HMp.
-  { destruct (modality_persistent_spec M) eqn:?; tac_modal_cases fi.
-    + by rewrite {1}affinely_elim_emp (modality_emp M)
-        persistently_True_emp affinely_persistently_emp.
-    + eauto using modality_persistent_forall_big_and.
-    + eauto using modality_persistent_transform,
-        modality_and_transform.
-    + by rewrite {1}affinely_elim_emp (modality_emp M)
-        persistently_True_emp affinely_persistently_emp.
-    + eauto using modality_persistent_id. }
-  move: HQ'; rewrite -HQ pure_True // left_id HMp=> HQ' {HQ Hwf HMp}.
-  destruct (modality_spatial_spec M) eqn:?; tac_modal_cases fi.
-  + 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)%I).
-  + rewrite -HQ' {1}(modality_spatial_id M ([∗] Γs')%I) //.
-    by rewrite -modality_sep.
-Qed.
-
 Lemma tac_modal_elim Δ Δ' i p φ P' P Q Q' :
   envs_lookup i Δ = Some (p, P) →
   ElimModal φ P P' Q Q' →
@@ -1206,6 +1064,176 @@ Proof.
 Qed.
 End bi_tactics.
 
+Class TransformPersistentEnv {PROP1 PROP2} (M : modality PROP1 PROP2)
+    (C : PROP2 → PROP1 → Prop) (Γin : env PROP2) (Γout : env PROP1) := {
+  transform_persistent_env :
+    (∀ P Q, C P Q → □ P ⊢ M (□ Q)) →
+    (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q)) →
+    □ ([∧] Γin) ⊢ M (□ ([∧] Γout));
+  transform_persistent_env_wf : env_wf Γin → env_wf Γout;
+  transform_persistent_env_dom i : Γin !! i = None → Γout !! i = None;
+}.
+
+Class TransformSpatialEnv {PROP1 PROP2} (M : modality PROP1 PROP2)
+    (C : PROP2 → PROP1 → Prop) (Γin : env PROP2) (Γout : env PROP1)
+    (filtered : bool) := {
+  transform_spatial_env :
+    (∀ P Q, C P Q → P ⊢ M Q) →
+    ([∗] Γin) ⊢ M ([∗] Γout) ∗ if filtered then True else emp;
+  transform_spatial_env_wf : env_wf Γin → env_wf Γout;
+  transform_spatial_env_dom i : Γin !! i = None → Γout !! i = None;
+}.
+
+Inductive IntoModalPersistentEnv {PROP2} : ∀ {PROP1} (M : modality PROP1 PROP2)
+    (Γin : env PROP2) (Γout : env PROP1), modality_intro_spec PROP1 PROP2 → Prop :=
+  | MIEnvIsEmpty_persistent {PROP1} (M : modality PROP1 PROP2) :
+     IntoModalPersistentEnv M Enil Enil MIEnvIsEmpty
+  | MIEnvForall_persistent (M : modality PROP2 PROP2) (C : PROP2 → Prop) Γ :
+     TCForall C (env_to_list Γ) →
+     IntoModalPersistentEnv M Γ Γ (MIEnvForall C)
+  | MIEnvTransform_persistent {PROP1}
+       (M : modality PROP1 PROP2) (C : PROP2 → PROP1 → Prop) Γin Γout :
+     TransformPersistentEnv M C Γin Γout →
+     IntoModalPersistentEnv M Γin Γout (MIEnvTransform C)
+  | MIEnvClear_persistent {PROP1 : bi} (M : modality PROP1 PROP2) Γ :
+     IntoModalPersistentEnv M Γ Enil MIEnvClear
+  | MIEnvId_persistent (M : modality PROP2 PROP2) Γ :
+     IntoModalPersistentEnv M Γ Γ MIEnvId.
+Existing Class IntoModalPersistentEnv.
+Existing Instances MIEnvIsEmpty_persistent MIEnvForall_persistent
+  MIEnvTransform_persistent MIEnvClear_persistent MIEnvId_persistent.
+
+Inductive IntoModalSpatialEnv {PROP2} : ∀ {PROP1} (M : modality PROP1 PROP2)
+    (Γin : env PROP2) (Γout : env PROP1), modality_intro_spec PROP1 PROP2 → bool → Prop :=
+  | MIEnvIsEmpty_spatial {PROP1} (M : modality PROP1 PROP2) :
+     IntoModalSpatialEnv M Enil Enil MIEnvIsEmpty false
+  | MIEnvForall_spatial (M : modality PROP2 PROP2) (C : PROP2 → Prop) Γ :
+     TCForall C (env_to_list Γ) →
+     IntoModalSpatialEnv M Γ Γ (MIEnvForall C) false
+  | MIEnvTransform_spatial {PROP1}
+       (M : modality PROP1 PROP2) (C : PROP2 → PROP1 → Prop) Γin Γout fi :
+     TransformSpatialEnv M C Γin Γout fi →
+     IntoModalSpatialEnv M Γin Γout (MIEnvTransform C) fi
+  | MIEnvClear_spatial {PROP1 : bi} (M : modality PROP1 PROP2) Γ :
+     IntoModalSpatialEnv M Γ Enil MIEnvClear false
+  | MIEnvId_spatial (M : modality PROP2 PROP2) Γ :
+     IntoModalSpatialEnv M Γ Γ MIEnvId false.
+Existing Class IntoModalSpatialEnv.
+Existing Instances MIEnvIsEmpty_spatial MIEnvForall_spatial
+  MIEnvTransform_spatial MIEnvClear_spatial MIEnvId_spatial.
+
+Section tac_modal_intro.
+  Context {PROP1 PROP2 : bi} (M : modality PROP1 PROP2).
+
+  Global Instance transform_persistent_env_nil C : TransformPersistentEnv M C Enil Enil.
+  Proof.
+    split; [|eauto using Enil_wf|done]=> /= ??.
+    rewrite !persistently_pure !affinely_True_emp.
+    by rewrite !affinely_emp -modality_emp.
+  Qed.
+  Global Instance transform_persistent_env_snoc (C : PROP2 → PROP1 → Prop) Γ Γ' i P Q :
+    C P Q →
+    TransformPersistentEnv M C Γ Γ' →
+    TransformPersistentEnv M C (Esnoc Γ i P) (Esnoc Γ' i Q).
+  Proof.
+    intros ? [HΓ Hwf Hdom]; split; simpl.
+    - intros HC Hand. rewrite affinely_persistently_and HC // HΓ //.
+      by rewrite Hand -affinely_persistently_and.
+    - inversion 1; constructor; auto.
+    - intros j. destruct (ident_beq _ _); naive_solver.
+  Qed.
+  Global Instance transform_persistent_env_snoc_not (C : PROP2 → PROP1 → Prop) Γ Γ' i P :
+    TransformPersistentEnv M C Γ Γ' →
+    TransformPersistentEnv M C (Esnoc Γ i P) Γ' | 100.
+  Proof.
+    intros [HΓ Hwf Hdom]; split; simpl.
+    - intros HC Hand. by rewrite and_elim_r HΓ.
+    - inversion 1; auto.
+    - intros j. destruct (ident_beq _ _); naive_solver.
+  Qed.
+
+  Global Instance transform_spatial_env_nil C :
+    TransformSpatialEnv M C Enil Enil false.
+  Proof.
+    split; [|eauto using Enil_wf|done]=> /= ?. by rewrite right_id -modality_emp.
+  Qed.
+  Global Instance transform_spatial_env_snoc (C : PROP2 → PROP1 → Prop) Γ Γ' i P Q fi :
+    C P Q →
+    TransformSpatialEnv M C Γ Γ' fi →
+    TransformSpatialEnv M C (Esnoc Γ i P) (Esnoc Γ' i Q) fi.
+  Proof.
+    intros ? [HΓ Hwf Hdom]; split; simpl.
+    - intros HC. by rewrite {1}(HC P) // HΓ // assoc modality_sep.
+    - inversion 1; constructor; auto.
+    - intros j. destruct (ident_beq _ _); naive_solver.
+  Qed.
+
+  Global Instance transform_spatial_env_snoc_not
+      (C : PROP2 → PROP1 → Prop) Γ Γ' i P fi fi' :
+    TransformSpatialEnv M C Γ Γ' fi →
+    TCIf (TCEq fi false)
+      (TCIf (Affine P) (TCEq fi' false) (TCEq fi' true))
+      (TCEq fi' true) →
+    TransformSpatialEnv M C (Esnoc Γ i P) Γ' fi' | 100.
+  Proof.
+    intros [HΓ Hwf Hdom] Hif; split; simpl.
+    - intros ?. rewrite HΓ //. destruct Hif as [-> [? ->| ->]| ->].
+      + by rewrite (affine P) left_id.
+      + by rewrite right_id comm (True_intro P).
+      + by rewrite comm -assoc (True_intro (_ ∗ P)%I).
+    - inversion 1; auto.
+    - intros j. destruct (ident_beq _ _); naive_solver.
+  Qed.
+
+  (** The actual introduction tactic *)
+  Lemma tac_modal_intro Γp Γs Γp' Γs' Q Q' fi :
+    FromModal M Q' Q →
+    IntoModalPersistentEnv M Γp Γp' (modality_persistent_spec M) →
+    IntoModalSpatialEnv M Γs Γs' (modality_spatial_spec M) fi →
+    (if fi then Absorbing Q' else TCTrue) →
+    envs_entails (Envs Γp' Γs') Q → envs_entails (Envs Γp Γs) Q'.
+  Proof.
+    rewrite envs_entails_eq /FromModal /of_envs /= => HQ' HΓp HΓs ? HQ.
+    apply pure_elim_l=> -[???]. assert (envs_wf (Envs Γp' Γs')) as Hwf.
+    { split; simpl in *.
+      - destruct HΓp as [| |????? []| |]; eauto using Enil_wf.
+      - destruct HΓs as [| |?????? []| |]; eauto using Enil_wf.
+      - assert (∀ i, Γp !! i = None → Γp' !! i = None).
+        { destruct HΓp as [| |????? []| |]; eauto. }
+        assert (∀ i, Γs !! i = None → Γs' !! i = None).
+        { destruct HΓs as [| |?????? []| |]; eauto. }
+        naive_solver. }
+    assert (□ [∧] Γp ⊢ M (□ [∧] Γp'))%I as HMp.
+    { remember (modality_persistent_spec M).
+      destruct HΓp as [?|M C Γp ?%TCForall_Forall|? M C Γp Γp' []|? M Γp|M Γp]; simpl.
+      - by rewrite {1}affinely_elim_emp (modality_emp M)
+          persistently_True_emp affinely_persistently_emp.
+      - eauto using modality_persistent_forall_big_and.
+      - eauto using modality_persistent_transform,
+          modality_and_transform.
+      - by rewrite {1}affinely_elim_emp (modality_emp M)
+          persistently_True_emp affinely_persistently_emp.
+      - eauto using modality_persistent_id. }
+    move: HQ'; rewrite -HQ pure_True // left_id HMp=> HQ' {HQ Hwf HMp}.
+    remember (modality_spatial_spec M).
+    destruct HΓs as [?|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)%I).
+    - rewrite -HQ' {1}(modality_spatial_id M ([∗] Γs)%I) //.
+      by rewrite -modality_sep.
+  Qed.
+End tac_modal_intro.
+
 Section sbi_tactics.
 Context {PROP : sbi}.
 Implicit Types Γ : env PROP.
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index b182599d4bc2fa2d8ba3d76b6ddfb438e6399385..df0833cd85c099aa20c89866f074b3fa6b45d452 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -21,7 +21,8 @@ Section modalities.
     modality_mixin (@monPred_absolutely I PROP)
       (MIEnvFilter Absolute) (MIEnvFilter Absolute).
   Proof.
-    split; split_and?; intros; try match goal with H : TCDiag _ _ _ |- _ => destruct H end;
+    split; simpl; split_and?; intros;
+      try match goal with H : TCDiag _ _ _ |- _ => destruct H end;
       eauto using bi.equiv_entails_sym, absolute_absolutely,
         monPred_absolutely_mono, monPred_absolutely_and,
         monPred_absolutely_sep_2 with typeclass_instances.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index ceca67932d7ca0be9452b75f4d2944cbecf5d0f3..3a0401699ffdcb7abc868a9316be8ee722c9a2cc 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -967,25 +967,21 @@ Tactic Notation "iModIntro":=
   eapply tac_modal_intro;
     [apply _  ||
      fail "iModIntro: the goal is not a modality"
-    |hnf; env_cbv;
-     apply _ ||
-     lazymatch goal with
-     | |- TCAnd (TCForall ?C _) _ => fail "iModIntro: persistent context does not satisfy" C
-     | |- TCAnd (TCEq _ Enil) _ => fail "iModIntro: persistent context is non-empty"
+    |apply _ ||
+     let s := lazymatch goal with |- IntoModalPersistentEnv _ _ _ ?s => s end in
+     lazymatch eval hnf in s with
+     | MIEnvForall ?C => fail "iModIntro: persistent context does not satisfy" C
+     | MIEnvIsEmpty => fail "iModIntro: persistent context is non-empty"
      end
-    |hnf; env_cbv;
-     lazymatch goal with
-     | |- ∃ _, TransformSpatialEnv _ _ _ _ _ ∧ _ =>
-        eexists; split;
-          [apply _
-          |apply _ || fail "iModIntro: cannot filter spatial context when goal is not absorbing"]
-     | |- TCAnd (TCForall ?C _) _ =>
-        apply _ || fail "iModIntro: spatial context does not satisfy" C
-     | |- TCAnd (TCEq _ Enil) _ =>
-        apply _ || fail "iModIntro: spatial context is non-empty"
-     | |- _ => apply _
+    |apply _ ||
+     let s := lazymatch goal with |- IntoModalPersistentEnv _ _ _ ?s => s end in
+     lazymatch eval hnf in s with
+     | MIEnvForall ?C => fail "iModIntro: spatial context does not satisfy" C
+     | MIEnvIsEmpty => fail "iModIntro: spatial context is non-empty"
      end
-    |env_cbv].
+    |env_cbv; apply _ ||
+     fail "iModIntro: cannot filter spatial context when goal is not absorbing"
+    |].
 Tactic Notation "iAlways" := iModIntro.
 
 (** * Later *)