diff --git a/ProofMode.md b/ProofMode.md
index 023a6d4c5ada2e32ed40f8fcb636bcb5c85227f0..7d8bd9b15e381ec3f8c7a36709c895d843da29a6 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -114,35 +114,26 @@ Separating logic specific tactics
 Modalities
 ----------
 
-- `iModIntro` : introduction of a modality that is an instance of the
-  `FromModal` type class. Instances include: later, except 0, basic update and
-  fancy update.
+- `iModIntro` : introduction of a modality. The type class `FromModal` is used
+  to specify which modalities this tactic should introduce. Instances of that
+  type class include: later, except 0, basic update and fancy update,
+  persistently, affinely, plainly, absorbingly, absolutely, and relatively.
+- `iAlways` : a deprecated alias of `iModIntro`.
+- `iNext n` : introduce `n` laters by stripping that number of laters from all
+  hypotheses. If the argument `n` is not given, it strips one later if the
+  leftmost conjunct is of the shape `â–· P`, or `n` laters if the leftmost
+  conjunct is of the shape `â–·^n P`.
 - `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality `pm_trm` that is
   an instance of the `ElimModal` type class. Instances include: later, except 0,
   basic update and fancy update.
 
-The persistence and plainness modalities
-----------------------------------------
-
-- `iAlways` : introduce a persistence or plainness modality and the spatial
-  context. In case of a plainness modality, the tactic will prune all persistent
-  hypotheses that are not plain.
-
-The later modality
-------------------
+Induction
+---------
 
-- `iNext n` : introduce `n` laters by stripping that number of laters from all
-  hypotheses. If the argument `n` is not given, it strips one later if the
-  leftmost conjunct is of the shape `â–· P`, or `n` laters if the leftmost
-  conjunct is of the shape `â–·^n P`.
 - `iLöb as "IH" forall (x1 ... xn) "selpat"` : perform Löb induction by
   generating a hypothesis `IH : â–· goal`. The tactic generalizes over the Coq
   level variables `x1 ... xn`, the hypotheses given by the selection pattern
   `selpat`, and the spatial context.
-
-Induction
----------
-
 - `iInduction x as cpat "IH" forall (x1 ... xn) "selpat"` : perform induction on
   the Coq term `x`. The Coq introduction pattern is used to name the introduced
   variables. The induction hypotheses are inserted into the persistent context
@@ -229,8 +220,8 @@ appear at the top level:
   Items of the selection pattern can be prefixed with `$`, which cause them to
   be framed instead of cleared.
 - `!%` : introduce a pure goal (and leave the proof mode).
-- `!#` : introduce an persistence or plainness modality (by calling `iAlways`).
-- `!>` : introduce a modality (by calling `iModIntro`).
+- `!>` : introduce a modality by calling `iModIntro`.
+- `!#` : introduce a modality by calling `iModIntro` (deprecated).
 - `/=` : perform `simpl`.
 - `//` : perform `try done` on all goals.
 - `//=` : syntactic sugar for `/= //`
diff --git a/_CoqProject b/_CoqProject
index c043f2d4544bf09bd2575c71e57dd492274a6392..623fce6cc6d71ffdc1b58419dff44ec34dd083dc 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -101,6 +101,8 @@ theories/proofmode/notation.v
 theories/proofmode/classes.v
 theories/proofmode/class_instances.v
 theories/proofmode/monpred.v
+theories/proofmode/modalities.v
+theories/proofmode/modality_instances.v
 theories/tests/heap_lang.v
 theories/tests/one_shot.v
 theories/tests/proofmode.v
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index f198601d096aa2d1a5fc9efe240e16775ec38d7f..3268cc849ef1d7e729fcae8694ab37c6f1f6e3bf 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -1,58 +1,88 @@
 From stdpp Require Import nat_cancel.
 From iris.bi Require Import bi tactics.
-From iris.proofmode Require Export classes.
+From iris.proofmode Require Export modality_instances classes.
 Set Default Proof Using "Type".
 Import bi.
 
-Section always_modalities.
+Section bi_modalities.
   Context {PROP : bi}.
-  Lemma always_modality_persistently_mixin :
-    always_modality_mixin (@bi_persistently PROP) AIEnvId AIEnvClear.
+
+  Lemma modality_persistently_mixin :
+    modality_mixin (@bi_persistently PROP) MIEnvId MIEnvClear.
   Proof.
-    split; eauto using equiv_entails_sym, persistently_intro, persistently_mono,
-      persistently_and, 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 always_modality_persistently :=
-    AlwaysModality _ always_modality_persistently_mixin.
+  Definition modality_persistently :=
+    Modality _ modality_persistently_mixin.
 
-  Lemma always_modality_affinely_mixin :
-    always_modality_mixin (@bi_affinely PROP) AIEnvId (AIEnvForall Affine).
+  Lemma modality_affinely_mixin :
+    modality_mixin (@bi_affinely PROP) MIEnvId (MIEnvForall Affine).
   Proof.
-    split; eauto using equiv_entails_sym, affinely_intro, affinely_mono,
-      affinely_and, affinely_sep_2 with typeclass_instances.
+    split; simpl; eauto using equiv_entails_sym, affinely_intro, affinely_mono,
+      affinely_sep_2 with typeclass_instances.
   Qed.
-  Definition always_modality_affinely :=
-    AlwaysModality _ always_modality_affinely_mixin.
+  Definition modality_affinely :=
+    Modality _ modality_affinely_mixin.
 
-  Lemma always_modality_affinely_persistently_mixin :
-    always_modality_mixin (λ P : PROP, □ P)%I AIEnvId AIEnvIsEmpty.
+  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_and, affinely_persistently_sep_2 with typeclass_instances.
+      affinely_persistently_sep_2 with typeclass_instances.
   Qed.
-  Definition always_modality_affinely_persistently :=
-    AlwaysModality _ always_modality_affinely_persistently_mixin.
+  Definition modality_affinely_persistently :=
+    Modality _ modality_affinely_persistently_mixin.
 
-  Lemma always_modality_plainly_mixin :
-    always_modality_mixin (@bi_plainly PROP) (AIEnvForall Plain) AIEnvClear.
+  Lemma modality_plainly_mixin :
+    modality_mixin (@bi_plainly PROP) (MIEnvForall Plain) MIEnvClear.
   Proof.
-    split; 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 always_modality_plainly :=
-    AlwaysModality _ always_modality_plainly_mixin.
+  Definition modality_plainly :=
+    Modality _ modality_plainly_mixin.
 
-  Lemma always_modality_affinely_plainly_mixin :
-    always_modality_mixin (λ P : PROP, ■ P)%I (AIEnvForall Plain) AIEnvIsEmpty.
+  Lemma modality_affinely_plainly_mixin :
+    modality_mixin (λ P : PROP, ■ P)%I (MIEnvForall Plain) MIEnvIsEmpty.
   Proof.
-    split; 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.
-  Definition always_modality_affinely_plainly :=
-    AlwaysModality _ always_modality_affinely_plainly_mixin.
-End always_modalities.
+  Definition modality_affinely_plainly :=
+    Modality _ modality_affinely_plainly_mixin.
+
+  Lemma modality_embed_mixin `{BiEmbedding PROP PROP'} :
+    modality_mixin (@bi_embed PROP PROP' _)
+      (MIEnvTransform IntoEmbed) (MIEnvTransform IntoEmbed).
+  Proof.
+    split; simpl; split_and?;
+      eauto using equiv_entails_sym, bi_embed_emp, bi_embed_sep, bi_embed_and.
+    - intros P Q. rewrite /IntoEmbed=> ->.
+      by rewrite bi_embed_affinely bi_embed_persistently.
+    - by intros P Q ->.
+  Qed.
+  Definition modality_embed `{BiEmbedding PROP PROP'} :=
+    Modality _ modality_embed_mixin.
+End bi_modalities.
+
+Section sbi_modalities.
+  Context {PROP : sbi}.
+
+  Lemma modality_laterN_mixin n :
+    modality_mixin (@sbi_laterN PROP n)
+      (MIEnvTransform (MaybeIntoLaterN false n)) (MIEnvTransform (MaybeIntoLaterN false n)).
+  Proof.
+    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 :=
+    Modality _ (modality_laterN_mixin n).
+End sbi_modalities.
 
 Section bi_instances.
 Context {PROP : bi}.
@@ -267,54 +297,54 @@ Global Instance into_persistent_persistent P :
   Persistent P → IntoPersistent false P P | 100.
 Proof. intros. by rewrite /IntoPersistent. Qed.
 
-(* FromAlways *)
-Global Instance from_always_affinely P :
-  FromAlways always_modality_affinely (bi_affinely P) P | 2.
-Proof. by rewrite /FromAlways. Qed.
-
-Global Instance from_always_persistently P :
-  FromAlways always_modality_persistently (bi_persistently P) P | 2.
-Proof. by rewrite /FromAlways. Qed.
-Global Instance from_always_affinely_persistently P :
-  FromAlways always_modality_affinely_persistently (â–¡ P) P | 1.
-Proof. by rewrite /FromAlways. Qed.
-Global Instance from_always_affinely_persistently_affine_bi P :
-  BiAffine PROP → FromAlways always_modality_persistently (□ P) P | 0.
-Proof. intros. by rewrite /FromAlways /= affine_affinely. Qed.
-
-Global Instance from_always_plainly P :
-  FromAlways always_modality_plainly (bi_plainly P) P | 2.
-Proof. by rewrite /FromAlways. Qed.
-Global Instance from_always_affinely_plainly P :
-  FromAlways always_modality_affinely_plainly (â–  P) P | 1.
-Proof. by rewrite /FromAlways. Qed.
-Global Instance from_always_affinely_plainly_affine_bi P :
-  BiAffine PROP → FromAlways always_modality_plainly (■ P) P | 0.
-Proof. intros. by rewrite /FromAlways /= affine_affinely. Qed.
-
-Global Instance from_always_affinely_embed `{BiEmbedding PROP PROP'} P Q :
-  FromAlways always_modality_affinely P Q →
-  FromAlways always_modality_affinely ⎡P⎤ ⎡Q⎤.
-Proof. rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely. Qed.
-Global Instance from_always_persistently_embed `{BiEmbedding PROP PROP'} P Q :
-  FromAlways always_modality_persistently P Q →
-  FromAlways always_modality_persistently ⎡P⎤ ⎡Q⎤.
-Proof. rewrite /FromAlways /= =><-. by rewrite bi_embed_persistently. Qed.
-Global Instance from_always_affinely_persistently_embed `{BiEmbedding PROP PROP'} P Q :
-  FromAlways always_modality_affinely_persistently P Q →
-  FromAlways always_modality_affinely_persistently ⎡P⎤ ⎡Q⎤.
-Proof.
-  rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely bi_embed_persistently.
-Qed.
-Global Instance from_always_plainly_embed `{BiEmbedding PROP PROP'} P Q :
-  FromAlways always_modality_plainly P Q →
-  FromAlways always_modality_plainly ⎡P⎤ ⎡Q⎤.
-Proof. rewrite /FromAlways /= =><-. by rewrite bi_embed_plainly. Qed.
-Global Instance from_always_affinely_plainly_embed `{BiEmbedding PROP PROP'} P Q :
-  FromAlways always_modality_affinely_plainly P Q →
-  FromAlways always_modality_affinely_plainly ⎡P⎤ ⎡Q⎤.
-Proof.
-  rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely bi_embed_plainly.
+(* FromModal *)
+Global Instance from_modal_affinely P :
+  FromModal modality_affinely (bi_affinely P) P | 2.
+Proof. by rewrite /FromModal. Qed.
+
+Global Instance from_modal_persistently P :
+  FromModal modality_persistently (bi_persistently P) P | 2.
+Proof. by rewrite /FromModal. Qed.
+Global Instance from_modal_affinely_persistently P :
+  FromModal modality_affinely_persistently (â–¡ P) P | 1.
+Proof. by rewrite /FromModal. Qed.
+Global Instance from_modal_affinely_persistently_affine_bi P :
+  BiAffine PROP → FromModal modality_persistently (□ P) P | 0.
+Proof. intros. by rewrite /FromModal /= affine_affinely. Qed.
+
+Global Instance from_modal_plainly P :
+  FromModal modality_plainly (bi_plainly P) P | 2.
+Proof. by rewrite /FromModal. Qed.
+Global Instance from_modal_affinely_plainly P :
+  FromModal modality_affinely_plainly (â–  P) P | 1.
+Proof. by rewrite /FromModal. Qed.
+Global Instance from_modal_affinely_plainly_affine_bi P :
+  BiAffine PROP → FromModal modality_plainly (■ P) P | 0.
+Proof. intros. by rewrite /FromModal /= affine_affinely. Qed.
+
+Global Instance from_modal_affinely_embed `{BiEmbedding PROP PROP'} P Q :
+  FromModal modality_affinely P Q →
+  FromModal modality_affinely ⎡P⎤ ⎡Q⎤.
+Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_affinely. Qed.
+Global Instance from_modal_persistently_embed `{BiEmbedding PROP PROP'} P Q :
+  FromModal modality_persistently P Q →
+  FromModal modality_persistently ⎡P⎤ ⎡Q⎤.
+Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_persistently. Qed.
+Global Instance from_modal_affinely_persistently_embed `{BiEmbedding PROP PROP'} P Q :
+  FromModal modality_affinely_persistently P Q →
+  FromModal modality_affinely_persistently ⎡P⎤ ⎡Q⎤.
+Proof.
+  rewrite /FromModal /= =><-. by rewrite bi_embed_affinely bi_embed_persistently.
+Qed.
+Global Instance from_modal_plainly_embed `{BiEmbedding PROP PROP'} P Q :
+  FromModal modality_plainly P Q →
+  FromModal modality_plainly ⎡P⎤ ⎡Q⎤.
+Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_plainly. Qed.
+Global Instance from_modal_affinely_plainly_embed `{BiEmbedding PROP PROP'} P Q :
+  FromModal modality_affinely_plainly P Q →
+  FromModal modality_affinely_plainly ⎡P⎤ ⎡Q⎤.
+Proof.
+  rewrite /FromModal /= =><-. by rewrite bi_embed_affinely bi_embed_plainly.
 Qed.
 
 (* IntoWand *)
@@ -1077,11 +1107,19 @@ Proof.
 Qed.
 
 (* FromModal *)
-Global Instance from_modal_absorbingly P : FromModal (bi_absorbingly P) P.
-Proof. apply absorbingly_intro. Qed.
-Global Instance from_modal_embed `{BiEmbedding PROP PROP'} P Q :
-  FromModal P Q → FromModal ⎡P⎤ ⎡Q⎤.
-Proof. by rewrite /FromModal=> ->. Qed.
+Global Instance from_modal_absorbingly P :
+  FromModal modality_id (bi_absorbingly P) P.
+Proof. by rewrite /FromModal /= -absorbingly_intro. Qed.
+Global Instance from_modal_embed `{BiEmbedding PROP PROP'} (P : PROP) :
+  FromModal (@modality_embed PROP PROP' _ _) ⎡P⎤ P.
+Proof. by rewrite /FromModal. Qed.
+
+(* ElimModal *)
+
+(* IntoEmbed *)
+Global Instance into_embed_embed {PROP' : bi} `{BiEmbed PROP PROP'} P :
+  IntoEmbed ⎡P⎤ P.
+Proof. by rewrite /IntoEmbed. Qed.
 
 (* AsValid *)
 Global Instance as_valid_valid {PROP : bi} (P : PROP) : AsValid0 (bi_valid P) P | 0.
@@ -1410,15 +1448,20 @@ Global Instance is_except_0_fupd `{FUpdFacts PROP} E1 E2 P :
 Proof. by rewrite /IsExcept0 except_0_fupd. Qed.
 
 (* FromModal *)
-Global Instance from_modal_later P : FromModal (â–· P) P.
-Proof. apply later_intro. Qed.
-Global Instance from_modal_except_0 P : FromModal (â—‡ P) P.
-Proof. apply except_0_intro. Qed.
-
-Global Instance from_modal_bupd `{BUpdFacts PROP} P : FromModal (|==> P) P.
-Proof. apply bupd_intro. Qed.
-Global Instance from_modal_fupd E P `{FUpdFacts PROP} : FromModal (|={E}=> P) P.
-Proof. rewrite /FromModal. apply fupd_intro. Qed.
+Global Instance from_modal_later n P Q :
+  NoBackTrack (FromLaterN n P Q) →
+  TCIf (TCEq n 0) False TCTrue →
+  FromModal (modality_laterN n) P Q | 100.
+Proof. rewrite /FromLaterN /FromModal. by intros [?] [_ []|?]. Qed.
+Global Instance from_modal_except_0 P : FromModal modality_id (â—‡ P) P.
+Proof. by rewrite /FromModal /= -except_0_intro. Qed.
+
+Global Instance from_modal_bupd `{BUpdFacts PROP} P :
+  FromModal modality_id (|==> P) P.
+Proof. by rewrite /FromModal /= -bupd_intro. Qed.
+Global Instance from_modal_fupd E P `{FUpdFacts PROP} :
+  FromModal modality_id (|={E}=> P) P.
+Proof. by rewrite /FromModal /= -fupd_intro. Qed.
 
 (* IntoInternalEq *)
 Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 4705cb3266c3566a84a312f10d103e6e0d78965b..09217c4f8b64fd7c267950b784a4109b4d51876c 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -1,4 +1,5 @@
 From iris.bi Require Export bi.
+From iris.proofmode Require Export modalities.
 From stdpp Require Import namespaces.
 Set Default Proof Using "Type".
 Import bi.
@@ -83,138 +84,22 @@ Arguments IntoPersistent {_} _ _%I _%I : simpl never.
 Arguments into_persistent {_} _ _%I _%I {_}.
 Hint Mode IntoPersistent + + ! - : typeclass_instances.
 
-(* The `iAlways` tactic is not tied to `persistently` and `affinely`, but can be
-instantiated with a variety of comonadic (always-style) modalities.
-
-In order to plug in an always-style modality, one has to decide for both the
-persistent and spatial what action should be performed upon introducing the
-modality:
-
-- Introduction is only allowed when the context is empty.
-- Introduction is only allowed when all hypotheses satisfy some predicate
-  `C : PROP → Prop` (where `C` should be a type class).
-- Introduction will only keep the hypotheses that satisfy some predicate
-  `C : PROP → Prop` (where `C` should be a type class).
-- Introduction will clear the context.
-- Introduction will keep the context as-if.
-
-Formally, these actions correspond to the following inductive type: *)
-Inductive always_intro_spec (PROP : bi) :=
-  | AIEnvIsEmpty
-  | AIEnvForall (C : PROP → Prop)
-  | AIEnvFilter (C : PROP → Prop)
-  | AIEnvClear
-  | AIEnvId.
-Arguments AIEnvIsEmpty {_}.
-Arguments AIEnvForall {_} _.
-Arguments AIEnvFilter {_} _.
-Arguments AIEnvClear {_}.
-Arguments AIEnvId {_}.
-
-(* An always-style modality is then a record packing together the modality with
-the laws it should satisfy to justify the given actions for both contexts: *)
-Record always_modality_mixin {PROP : bi} (M : PROP → PROP)
-    (pspec sspec : always_intro_spec PROP) := {
-  always_modality_mixin_persistent :
-    match pspec with
-    | AIEnvIsEmpty => True
-    | AIEnvForall C | AIEnvFilter C => ∀ P, C P → □ P ⊢ M (□ P)
-    | AIEnvClear => True
-    | AIEnvId => ∀ P, □ P ⊢ M (□ P)
-    end;
-  always_modality_mixin_spatial :
-    match sspec with
-    | AIEnvIsEmpty => True
-    | AIEnvForall C => ∀ P, C P → P ⊢ M P
-    | AIEnvFilter C => (∀ P, C P → P ⊢ M P) ∧ (∀ P, Absorbing (M P))
-    | AIEnvClear => ∀ P, Absorbing (M P)
-    | AIEnvId => False
-    end;
-  always_modality_mixin_emp : emp ⊢ M emp;
-  always_modality_mixin_mono P Q : (P ⊢ Q) → M P ⊢ M Q;
-  always_modality_mixin_and P Q : M P ∧ M Q ⊢ M (P ∧ Q);
-  always_modality_mixin_sep P Q : M P ∗ M Q ⊢ M (P ∗ Q)
-}.
-
-Record always_modality (PROP : bi) := AlwaysModality {
-  always_modality_car :> PROP → PROP;
-  always_modality_persistent_spec : always_intro_spec PROP;
-  always_modality_spatial_spec : always_intro_spec PROP;
-  always_modality_mixin_of : always_modality_mixin
-    always_modality_car
-    always_modality_persistent_spec always_modality_spatial_spec
-}.
-Arguments AlwaysModality {_} _ {_ _} _.
-Arguments always_modality_persistent_spec {_} _.
-Arguments always_modality_spatial_spec {_} _.
-
-Section always_modality.
-  Context {PROP} (M : always_modality PROP).
-
-  Lemma always_modality_persistent_forall C P :
-    always_modality_persistent_spec M = AIEnvForall C → C P → □ P ⊢ M (□ P).
-  Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_persistent_filter C P :
-    always_modality_persistent_spec M = AIEnvFilter C → C P → □ P ⊢ M (□ P).
-  Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_persistent_id P :
-    always_modality_persistent_spec M = AIEnvId → □ P ⊢ M (□ P).
-  Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_spatial_forall C P :
-    always_modality_spatial_spec M = AIEnvForall C → C P → P ⊢ M P.
-  Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_spatial_filter C P :
-    always_modality_spatial_spec M = AIEnvFilter C → C P → P ⊢ M P.
-  Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_spatial_filter_absorbing C P :
-    always_modality_spatial_spec M = AIEnvFilter C → Absorbing (M P).
-  Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_spatial_clear P :
-    always_modality_spatial_spec M = AIEnvClear → Absorbing (M P).
-  Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_spatial_id :
-    always_modality_spatial_spec M ≠ AIEnvId.
-  Proof. destruct M as [??? []]; naive_solver. Qed.
-
-  Lemma always_modality_emp : emp ⊢ M emp.
-  Proof. eapply always_modality_mixin_emp, always_modality_mixin_of. Qed.
-  Lemma always_modality_mono P Q : (P ⊢ Q) → M P ⊢ M Q.
-  Proof. eapply always_modality_mixin_mono, always_modality_mixin_of. Qed.
-  Lemma always_modality_and P Q : M P ∧ M Q ⊢ M (P ∧ Q).
-  Proof. eapply always_modality_mixin_and, always_modality_mixin_of. Qed.
-  Lemma always_modality_sep P Q : M P ∗ M Q ⊢ M (P ∗ Q).
-  Proof. eapply always_modality_mixin_sep, always_modality_mixin_of. Qed.
-  Global Instance always_modality_mono' : Proper ((⊢) ==> (⊢)) M.
-  Proof. intros P Q. apply always_modality_mono. Qed.
-  Global Instance always_modality_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) M.
-  Proof. intros P Q. apply always_modality_mono. Qed.
-  Global Instance always_modality_proper : Proper ((≡) ==> (≡)) M.
-  Proof. intros P Q. rewrite !equiv_spec=> -[??]; eauto using always_modality_mono. Qed.
-
-  Lemma always_modality_persistent_forall_big_and C Ps :
-    always_modality_persistent_spec M = AIEnvForall C →
-    Forall C Ps → □ [∧] Ps ⊢ M (□ [∧] Ps).
-  Proof.
-    induction 2 as [|P Ps ? _ IH]; simpl.
-    - by rewrite persistently_pure affinely_True_emp affinely_emp -always_modality_emp.
-    - rewrite affinely_persistently_and -always_modality_and -IH.
-      by rewrite {1}(always_modality_persistent_forall _ P).
-  Qed.
-  Lemma always_modality_spatial_forall_big_sep C Ps :
-    always_modality_spatial_spec M = AIEnvForall C →
-    Forall C Ps → [∗] Ps ⊢ M ([∗] Ps).
-  Proof.
-    induction 2 as [|P Ps ? _ IH]; simpl.
-    - by rewrite -always_modality_emp.
-    - by rewrite -always_modality_sep -IH {1}(always_modality_spatial_forall _ P).
-  Qed.
-End always_modality.
-
-Class FromAlways {PROP : bi} (M : always_modality PROP) (P Q : PROP) :=
-  from_always : M Q ⊢ P.
-Arguments FromAlways {_} _ _%I _%I : simpl never.
-Arguments from_always {_} _ _%I _%I {_}.
-Hint Mode FromAlways + - ! - : typeclass_instances.
+(** The [FromModal M P Q] class is used by the [iModIntro] tactic to transform
+a goal [P] into a modality [M] and proposition [Q].
+
+The input is [P] and the outputs are [M] and [Q].
+
+For modalities [M] that do not need to augment the proof mode environment, one
+can define an instance [FromModal modality_id (M P) P]. Defining such an
+only imposes the proof obligation [P ⊢ M P]. Examples of modalities that have
+such an instance are [bupd], [fupd], [except_0], [monPred_relatively] and
+[bi_absorbingly]. *)
+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.
 
 Class FromAffinely {PROP : bi} (P Q : PROP) :=
   from_affinely : bi_affinely Q ⊢ P.
@@ -332,11 +217,6 @@ Arguments IsExcept0 {_} _%I : simpl never.
 Arguments is_except_0 {_} _%I {_}.
 Hint Mode IsExcept0 + ! : typeclass_instances.
 
-Class FromModal {PROP : bi} (P Q : PROP) := from_modal : Q ⊢ P.
-Arguments FromModal {_} _%I _%I : simpl never.
-Arguments from_modal {_} _%I _%I {_}.
-Hint Mode FromModal + ! - : typeclass_instances.
-
 Class ElimModal {PROP : bi} (φ : Prop) (P P' : PROP) (Q Q' : PROP) :=
   elim_modal : φ → P ∗ (P' -∗ Q') ⊢ Q.
 Arguments ElimModal {_} _ _%I _%I _%I _%I : simpl never.
@@ -553,6 +433,16 @@ Arguments FromLaterN {_} _%nat_scope _%I _%I.
 Arguments from_laterN {_} _%nat_scope _%I _%I {_}.
 Hint Mode FromLaterN + - ! - : typeclass_instances.
 
+(** The class [IntoEmbed P Q] is used to transform hypotheses while introducing
+embeddings using [iModIntro].
+
+Input: the proposition [P], output: the proposition [Q] so that [P ⊢ ⎡Q⎤] *)
+Class IntoEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP') (Q : PROP) :=
+  into_embed : P ⊢ ⎡Q⎤.
+Arguments IntoEmbed {_ _ _} _%I _%I.
+Arguments into_embed {_ _ _} _%I _%I {_}.
+Hint Mode IntoEmbed + + + ! -  : typeclass_instances.
+
 (* We use two type classes for [AsValid], in order to avoid loops in
    typeclass search. Indeed, the [as_valid_embed] instance would try
    to add an arbitrary number of embeddings. To avoid this, the
@@ -644,8 +534,8 @@ Instance into_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
   IntoExist P Φ → IntoExist (tc_opaque P) Φ := id.
 Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (tc_opaque P) Φ := id.
-Instance from_modal_tc_opaque {PROP : bi} (P Q : PROP) :
-  FromModal P Q → FromModal (tc_opaque P) Q := id.
+Instance from_modal_tc_opaque {PROP : bi} M (P Q : PROP) :
+  FromModal M P Q → FromModal M (tc_opaque P) Q := id.
 Instance elim_modal_tc_opaque {PROP : bi} φ (P P' Q Q' : PROP) :
   ElimModal φ P P' Q Q' → ElimModal φ (tc_opaque P) P' Q Q' := id.
 Instance into_inv_tc_opaque {PROP : bi} (P : PROP) N :
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 840d129b0194424968ca9e44f40b46e103e5d48d..266c806795dd59256cb2a66906bb8a8b61acaee1 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -1,6 +1,6 @@
 From iris.bi Require Export bi.
 From iris.bi Require Import tactics.
-From iris.proofmode Require Export base environments classes.
+From iris.proofmode Require Export base environments classes modality_instances.
 Set Default Proof Using "Type".
 Import bi.
 Import env_notations.
@@ -583,126 +583,7 @@ Qed.
 Lemma tac_pure_revert Δ φ Q : envs_entails Δ (⌜φ⌝ → Q) → (φ → envs_entails Δ Q).
 Proof. rewrite envs_entails_eq. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
 
-(** * Always modalities *)
-Class FilterPersistentEnv
-    (M : always_modality PROP) (C : PROP → Prop) (Γ1 Γ2 : env PROP) := {
-  filter_persistent_env :
-    (∀ P, C P → □ P ⊢ M (□ P)) →
-    □ ([∧] Γ1) ⊢ M (□ ([∧] Γ2));
-  filter_persistent_env_wf : env_wf Γ1 → env_wf Γ2;
-  filter_persistent_env_dom i : Γ1 !! i = None → Γ2 !! i = None;
-}.
-Global Instance filter_persistent_env_nil M C : FilterPersistentEnv M C Enil Enil.
-Proof.
-  split=> // HC /=. rewrite !persistently_pure !affinely_True_emp.
-  by rewrite affinely_emp -always_modality_emp.
-Qed.
-Global Instance filter_persistent_env_snoc M (C : PROP → Prop) Γ Γ' i P :
-  C P →
-  FilterPersistentEnv M C Γ Γ' →
-  FilterPersistentEnv M C (Esnoc Γ i P) (Esnoc Γ' i P).
-Proof.
-  intros ? [HΓ Hwf Hdom]; split; simpl.
-  - intros HC. rewrite affinely_persistently_and HC // HΓ //.
-    by rewrite always_modality_and -affinely_persistently_and.
-  - inversion 1; constructor; auto.
-  - intros j. destruct (ident_beq _ _); naive_solver.
-Qed.
-Global Instance filter_persistent_env_snoc_not M (C : PROP → Prop) Γ Γ' i P :
-  FilterPersistentEnv M C Γ Γ' →
-  FilterPersistentEnv M C (Esnoc Γ i P) Γ' | 100.
-Proof.
-  intros [HΓ Hwf Hdom]; split; simpl.
-  - intros HC. by rewrite and_elim_r HΓ.
-  - inversion 1; auto.
-  - intros j. destruct (ident_beq _ _); naive_solver.
-Qed.
-
-Class FilterSpatialEnv
-    (M : always_modality PROP) (C : PROP → Prop) (Γ1 Γ2 : env PROP) := {
-  filter_spatial_env :
-    (∀ P, C P → P ⊢ M P) → (∀ P, Absorbing (M P)) →
-    ([∗] Γ1) ⊢ M ([∗] Γ2);
-  filter_spatial_env_wf : env_wf Γ1 → env_wf Γ2;
-  filter_spatial_env_dom i : Γ1 !! i = None → Γ2 !! i = None;
-}.
-Global Instance filter_spatial_env_nil M C : FilterSpatialEnv M C Enil Enil.
-Proof. split=> // HC /=. by rewrite -always_modality_emp. Qed.
-Global Instance filter_spatial_env_snoc M (C : PROP → Prop) Γ Γ' i P :
-  C P →
-  FilterSpatialEnv M C Γ Γ' →
-  FilterSpatialEnv M C (Esnoc Γ i P) (Esnoc Γ' i P).
-Proof.
-  intros ? [HΓ Hwf Hdom]; split; simpl.
-  - intros HC ?. by rewrite {1}(HC P) // HΓ // always_modality_sep.
-  - inversion 1; constructor; auto.
-  - intros j. destruct (ident_beq _ _); naive_solver.
-Qed.
-
-Global Instance filter_spatial_env_snoc_not M (C : PROP → Prop) Γ Γ' i P :
-  FilterSpatialEnv M C Γ Γ' →
-  FilterSpatialEnv M C (Esnoc Γ i P) Γ' | 100.
-Proof.
-  intros [HΓ Hwf Hdom]; split; simpl.
-  - intros HC ?. by rewrite HΓ // sep_elim_r.
-  - inversion 1; auto.
-  - intros j. destruct (ident_beq _ _); naive_solver.
-Qed.
-
-Ltac tac_always_cases :=
-  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 : FilterPersistentEnv _ _ _ _ |- _ => destruct H
-  | H : FilterSpatialEnv _ _ _ _ |- _ => destruct H
-  end; simpl; auto using Enil_wf.
-
-Lemma tac_always_intro Γp Γs Γp' Γs' M Q Q' :
-  FromAlways M Q' Q →
-  match always_modality_persistent_spec M with
-  | AIEnvForall C => TCAnd (TCForall C (env_to_list Γp)) (TCEq Γp Γp')
-  | AIEnvFilter C => FilterPersistentEnv M C Γp Γp'
-  | AIEnvIsEmpty => TCAnd (TCEq Γp Enil) (TCEq Γp' Enil)
-  | AIEnvClear => TCEq Γp' Enil
-  | AIEnvId => TCEq Γp Γp'
-  end →
-  match always_modality_spatial_spec M with
-  | AIEnvForall C => TCAnd (TCForall C (env_to_list Γs)) (TCEq Γs Γs')
-  | AIEnvFilter C => FilterSpatialEnv M C Γs Γs'
-  | AIEnvIsEmpty => TCAnd (TCEq Γs Enil) (TCEq Γs' Enil)
-  | AIEnvClear => TCEq Γs' Enil
-  | AIEnvId => TCEq Γs Γs'
-  end →
-  envs_entails (Envs Γp' Γs') Q → envs_entails (Envs Γp Γs) Q'.
-Proof.
-  rewrite envs_entails_eq /FromAlways /of_envs /= => <- HΓp HΓs <-.
-  apply pure_elim_l=> -[???]. assert (envs_wf (Envs Γp' Γs')).
-  { split; simpl in *.
-    - destruct (always_modality_persistent_spec M); tac_always_cases.
-    - destruct (always_modality_spatial_spec M); tac_always_cases.
-    - destruct (always_modality_persistent_spec M),
-        (always_modality_spatial_spec M); tac_always_cases; naive_solver. }
-  rewrite pure_True // left_id. rewrite -always_modality_sep. apply sep_mono.
-  - destruct (always_modality_persistent_spec M) eqn:?; tac_always_cases.
-    + by rewrite {1}affinely_elim_emp (always_modality_emp M)
-        persistently_True_emp affinely_persistently_emp.
-    + eauto using always_modality_persistent_forall_big_and.
-    + eauto using always_modality_persistent_filter.
-    + by rewrite {1}affinely_elim_emp (always_modality_emp M)
-        persistently_True_emp affinely_persistently_emp.
-    + eauto using always_modality_persistent_id.
-  - destruct (always_modality_spatial_spec M) eqn:?; tac_always_cases.
-    + by rewrite -always_modality_emp.
-    + eauto using always_modality_spatial_forall_big_sep.
-    + eauto using always_modality_spatial_filter,
-        always_modality_spatial_filter_absorbing.
-    + rewrite -(always_modality_spatial_clear M) // -always_modality_emp.
-      by rewrite -absorbingly_True_emp absorbingly_pure -True_intro.
-    + by destruct (always_modality_spatial_id M).
-Qed.
-
+(** * Persistence *)
 Lemma tac_persistent Δ Δ' i p P P' Q :
   envs_lookup i Δ = Some (p, P) →
   IntoPersistent p P P' →
@@ -1155,10 +1036,6 @@ Proof.
 Qed.
 
 (** * Modalities *)
-Lemma tac_modal_intro Δ P Q :
-  FromModal P Q → envs_entails Δ Q → envs_entails Δ P.
-Proof. by rewrite envs_entails_eq /FromModal=> <- ->. Qed.
-
 Lemma tac_modal_elim Δ Δ' i p φ P' P Q Q' :
   envs_lookup i Δ = Some (p, P) →
   ElimModal φ P P' Q Q' →
@@ -1187,6 +1064,229 @@ Proof.
 Qed.
 End bi_tactics.
 
+(** The following _private_ classes are used internally by [tac_modal_intro] /
+[iModIntro] to transform the proofmode environments when introducing a modality.
+
+The class [TransformPersistentEnv M C Γin Γout] is used to transform the
+persistent environment using a type class [C].
+
+Inputs:
+- [Γin] : the original environment.
+- [M] : the modality that the environment should be transformed into.
+- [C : PROP → PROP → Prop] : a type class that is used to transform the
+  individual hypotheses. The first parameter is the input and the second
+  parameter is the output.
+
+Outputs:
+- [Γout] : the resulting environment. *)
+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;
+}.
+
+(* The class [TransformPersistentEnv M C Γin Γout filtered] is used to transform
+the persistent environment using a type class [C].
+
+Inputs:
+- [Γin] : the original environment.
+- [M] : the modality that the environment should be transformed into.
+- [C : PROP → PROP → Prop] : a type class that is used to transform the
+  individual hypotheses. The first parameter is the input and the second
+  parameter is the output.
+
+Outputs:
+- [Γout] : the resulting environment.
+- [filtered] : a Boolean indicating if non-affine hypotheses have been cleared. *)
+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;
+}.
+
+(* The class [IntoModalPersistentEnv M Γin Γout s] is used to transform the
+persistent environment with respect to the behavior needed to introduce [M] as
+given by [s : modality_intro_spec PROP1 PROP2].
+
+Inputs:
+- [Γin] : the original environment.
+- [M] : the modality that the environment should be transformed into.
+- [s] : the [modality_intro_spec] a specification of the way the hypotheses
+  should be transformed.
+
+Outputs:
+- [Γout] : the resulting environment. *)
+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.
+
+(* The class [IntoModalSpatialEnv M Γin Γout s] is used to transform the spatial
+environment with respect to the behavior needed to introduce [M] as given by
+[s : modality_intro_spec PROP1 PROP2].
+
+Inputs:
+- [Γin] : the original environment.
+- [M] : the modality that the environment should be transformed into.
+- [s] : the [modality_intro_spec] a specification of the way the hypotheses
+  should be transformed.
+
+Outputs:
+- [Γout] : the resulting environment.
+- [filtered] : a Boolean indicating if non-affine hypotheses have been cleared. *)
+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.
@@ -1231,44 +1331,33 @@ Proof.
 Qed.
 
 (** * Later *)
-Class MaybeIntoLaterNEnv (n : nat) (Γ1 Γ2 : env PROP) :=
-  into_laterN_env : env_Forall2 (MaybeIntoLaterN false n) Γ1 Γ2.
+(** The class [MaybeIntoLaterNEnvs] is used by tactics that need to introduce
+laters, e.g. the symbolic execution tactics. *)
 Class MaybeIntoLaterNEnvs (n : nat) (Δ1 Δ2 : envs PROP) := {
-  into_later_persistent:  MaybeIntoLaterNEnv n (env_persistent Δ1) (env_persistent Δ2);
-  into_later_spatial: MaybeIntoLaterNEnv n (env_spatial Δ1) (env_spatial Δ2)
+  into_later_persistent :
+    TransformPersistentEnv (modality_laterN n) (MaybeIntoLaterN false n)
+      (env_persistent Δ1) (env_persistent Δ2);
+  into_later_spatial :
+    TransformSpatialEnv (modality_laterN n)
+      (MaybeIntoLaterN false n) (env_spatial Δ1) (env_spatial Δ2) false
 }.
 
-Global Instance into_laterN_env_nil n : MaybeIntoLaterNEnv n Enil Enil.
-Proof. constructor. Qed.
-Global Instance into_laterN_env_snoc n Γ1 Γ2 i P Q :
-  MaybeIntoLaterNEnv n Γ1 Γ2 → MaybeIntoLaterN false n P Q →
-  MaybeIntoLaterNEnv n (Esnoc Γ1 i P) (Esnoc Γ2 i Q).
-Proof. by constructor. Qed.
-
 Global Instance into_laterN_envs n Γp1 Γp2 Γs1 Γs2 :
-  MaybeIntoLaterNEnv n Γp1 Γp2 → MaybeIntoLaterNEnv n Γs1 Γs2 →
+  TransformPersistentEnv (modality_laterN n) (MaybeIntoLaterN false n) Γp1 Γp2 →
+  TransformSpatialEnv (modality_laterN n) (MaybeIntoLaterN false n) Γs1 Γs2 false →
   MaybeIntoLaterNEnvs n (Envs Γp1 Γs1) (Envs Γp2 Γs2).
 Proof. by split. Qed.
 
 Lemma into_laterN_env_sound n Δ1 Δ2 :
   MaybeIntoLaterNEnvs n Δ1 Δ2 → of_envs Δ1 ⊢ ▷^n (of_envs Δ2).
 Proof.
-  intros [Hp Hs]; rewrite /of_envs /= !laterN_and !laterN_sep.
-  rewrite -{1}laterN_intro -laterN_affinely_persistently_2.
-  apply and_mono, sep_mono.
-  - apply pure_mono; destruct 1; constructor;
-      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
-  - apply affinely_mono, persistently_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.
-
-Lemma tac_next Δ Δ' n Q Q' :
-  FromLaterN n Q Q' → MaybeIntoLaterNEnvs n Δ Δ' →
-  envs_entails Δ' Q' → envs_entails Δ Q.
-Proof.
-  rewrite envs_entails_eq => ?? HQ.
-  by rewrite -(from_laterN n Q) into_laterN_env_sound HQ.
+  intros [[Hp ??] [Hs ??]]; rewrite /of_envs /= !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.
+    + intros P Q ->. by rewrite laterN_affinely_persistently_2.
+    + intros P Q. by rewrite laterN_and.
+  - by rewrite Hs //= right_id.
 Qed.
 
 Lemma tac_löb Δ Δ' i Q :
diff --git a/theories/proofmode/modalities.v b/theories/proofmode/modalities.v
new file mode 100644
index 0000000000000000000000000000000000000000..2ec838ca783a20824c23a26f13832360085a5179
--- /dev/null
+++ b/theories/proofmode/modalities.v
@@ -0,0 +1,160 @@
+From iris.bi Require Export bi.
+From stdpp Require Import namespaces.
+Set Default Proof Using "Type".
+Import bi.
+
+(** The `iModIntro` tactic is not tied the Iris modalities, but can be
+instantiated with a variety of modalities.
+
+In order to plug in a modality, one has to decide for both the persistent and
+spatial what action should be performed upon introducing the modality:
+
+- Introduction is only allowed when the context is empty.
+- Introduction is only allowed when all hypotheses satisfy some predicate
+  `C : PROP → Prop` (where `C` should be a type class).
+- Introduction will transform each hypotheses using a type class
+  `C : PROP → PROP → Prop`, where the first parameter is the input and the
+  second parameter is the output. Hypotheses that cannot be transformed (i.e.
+  for which no instance of `C` can be found) will be cleared.
+- Introduction will clear the context.
+- Introduction will keep the context as-if.
+
+Formally, these actions correspond to the following inductive type: *)
+
+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 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 {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 (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 {_ _} _.
+
+Section modality.
+  Context {PROP1 PROP2} (M : modality PROP1 PROP2).
+
+  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_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_emp : emp ⊢ M emp.
+  Proof. eapply modality_mixin_emp, modality_mixin_of. Qed.
+  Lemma modality_mono P Q : (P ⊢ Q) → M P ⊢ M Q.
+  Proof. eapply modality_mixin_mono, modality_mixin_of. Qed.
+  Lemma modality_sep P Q : M P ∗ M Q ⊢ M (P ∗ Q).
+  Proof. eapply modality_mixin_sep, modality_mixin_of. Qed.
+  Global Instance modality_mono' : Proper ((⊢) ==> (⊢)) M.
+  Proof. intros P Q. apply modality_mono. Qed.
+  Global Instance modality_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) M.
+  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 →
+    Forall C Ps → □ [∧] Ps ⊢ M (□ [∧] Ps).
+  Proof.
+    induction 2 as [|P Ps ? _ IH]; simpl.
+    - by rewrite persistently_pure affinely_True_emp affinely_emp -modality_emp.
+    - rewrite affinely_persistently_and -modality_and_forall // -IH.
+      by rewrite {1}(modality_persistent_forall _ P).
+  Qed.
+  Lemma modality_spatial_forall_big_sep C Ps :
+    modality_spatial_spec M = MIEnvForall C →
+    Forall C Ps → [∗] Ps ⊢ M ([∗] Ps).
+  Proof.
+    induction 2 as [|P Ps ? _ IH]; simpl.
+    - by rewrite -modality_emp.
+    - by rewrite -modality_sep -IH {1}(modality_spatial_forall _ P).
+  Qed.
+End modality1.
+
+(** The identity modality [modality_id] can be used in combination with
+[FromModal modality_id] to support introduction for modalities that enjoy
+[P ⊢ M P]. This is done by defining an instance [FromModal modality_id (M P) P],
+which will instruct [iModIntro] to introduce the modality without modifying the
+proof mode context. Examples of such modalities are [bupd], [fupd], [except_0],
+[monPred_relatively] and [bi_absorbingly]. *)
+Lemma modality_id_mixin {PROP : bi} : modality_mixin (@id PROP) MIEnvId MIEnvId.
+Proof. split; simpl; eauto. Qed.
+Definition modality_id {PROP : bi} := Modality (@id PROP) modality_id_mixin.
diff --git a/theories/proofmode/modality_instances.v b/theories/proofmode/modality_instances.v
new file mode 100644
index 0000000000000000000000000000000000000000..8fcfc827a9fa7e302292bc728f778235490eb5b9
--- /dev/null
+++ b/theories/proofmode/modality_instances.v
@@ -0,0 +1,84 @@
+From iris.bi Require Import bi.
+From iris.proofmode Require Export classes.
+Set Default Proof Using "Type".
+Import bi.
+
+Section bi_modalities.
+  Context {PROP : bi}.
+
+  Lemma modality_persistently_mixin :
+    modality_mixin (@bi_persistently PROP) MIEnvId MIEnvClear.
+  Proof.
+    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.
+
+  Lemma modality_affinely_mixin :
+    modality_mixin (@bi_affinely PROP) MIEnvId (MIEnvForall Affine).
+  Proof.
+    split; simpl; eauto using equiv_entails_sym, affinely_intro, affinely_mono,
+      affinely_sep_2 with typeclass_instances.
+  Qed.
+  Definition modality_affinely :=
+    Modality _ modality_affinely_mixin.
+
+  Lemma modality_affinely_persistently_mixin :
+    modality_mixin (λ P : PROP, □ P)%I MIEnvId MIEnvIsEmpty.
+  Proof.
+    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.
+  Definition modality_affinely_persistently :=
+    Modality _ modality_affinely_persistently_mixin.
+
+  Lemma modality_plainly_mixin :
+    modality_mixin (@bi_plainly PROP) (MIEnvForall Plain) MIEnvClear.
+  Proof.
+    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.
+
+  Lemma modality_affinely_plainly_mixin :
+    modality_mixin (λ P : PROP, ■ P)%I (MIEnvForall Plain) MIEnvIsEmpty.
+  Proof.
+    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.
+  Definition modality_affinely_plainly :=
+    Modality _ modality_affinely_plainly_mixin.
+
+  Lemma modality_embed_mixin `{BiEmbedding PROP PROP'} :
+    modality_mixin (@bi_embed PROP PROP' _)
+      (MIEnvTransform IntoEmbed) (MIEnvTransform IntoEmbed).
+  Proof.
+    split; simpl; split_and?;
+      eauto using equiv_entails_sym, bi_embed_emp, bi_embed_sep, bi_embed_and.
+    - intros P Q. rewrite /IntoEmbed=> ->.
+      by rewrite bi_embed_affinely bi_embed_persistently.
+    - by intros P Q ->.
+  Qed.
+  Definition modality_embed `{BiEmbedding PROP PROP'} :=
+    Modality _ modality_embed_mixin.
+End bi_modalities.
+
+Section sbi_modalities.
+  Context {PROP : sbi}.
+
+  Lemma modality_laterN_mixin n :
+    modality_mixin (@sbi_laterN PROP n)
+      (MIEnvTransform (MaybeIntoLaterN false n)) (MIEnvTransform (MaybeIntoLaterN false n)).
+  Proof.
+    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 :=
+    Modality _ (modality_laterN_mixin n).
+End sbi_modalities.
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index ae5a975dc089cc9b3a38037ff2257d87fae0457b..8554d1845594314fb7fd39ef559b1a1d5618b069 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -14,32 +14,22 @@ Proof. by rewrite /IsBiIndexRel. Qed.
 Hint Extern 1 (IsBiIndexRel _ _) => unfold IsBiIndexRel; assumption
             : typeclass_instances.
 
-Section always_modalities.
-Context {I : biIndex} {PROP : bi}.
+Section modalities.
+  Context {I : biIndex} {PROP : bi}.
 
-  Lemma always_modality_absolutely_mixin :
-    always_modality_mixin (@monPred_absolutely I PROP)
-      (AIEnvFilter Absolute) (AIEnvForall Absolute).
+  Lemma modality_absolutely_mixin :
+    modality_mixin (@monPred_absolutely I PROP)
+      (MIEnvFilter Absolute) (MIEnvFilter Absolute).
   Proof.
-    split; eauto using bi.equiv_entails_sym, absolute_absolutely,
-       monPred_absolutely_mono, monPred_absolutely_and,
-       monPred_absolutely_sep_2 with typeclass_instances.
+    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.
   Qed.
-  Definition always_modality_absolutely :=
-    AlwaysModality _ always_modality_absolutely_mixin.
-
-  (* We can only filter the spatial context in case the BI is affine *)
-  Lemma always_modality_absolutely_filter_spatial_mixin `{BiAffine PROP} :
-    always_modality_mixin (@monPred_absolutely I PROP)
-      (AIEnvFilter Absolute) (AIEnvFilter Absolute).
-  Proof.
-    split; eauto using bi.equiv_entails_sym, absolute_absolutely,
-       monPred_absolutely_mono, monPred_absolutely_and,
-       monPred_absolutely_sep_2 with typeclass_instances.
-  Qed.
-  Definition always_modality_absolutely_filter_spatial `{BiAffine PROP} :=
-    AlwaysModality _ always_modality_absolutely_filter_spatial_mixin.
-End always_modalities.
+  Definition modality_absolutely :=
+    Modality _ modality_absolutely_mixin.
+End modalities.
 
 Section bi.
 Context {I : biIndex} {PROP : bi}.
@@ -50,12 +40,12 @@ Implicit Types 𝓟 𝓠 𝓡 : PROP.
 Implicit Types φ : Prop.
 Implicit Types i j : I.
 
-Global Instance from_always_absolutely P :
-  FromAlways always_modality_absolutely (∀ᵢ P) P | 1.
-Proof. by rewrite /FromAlways. Qed.
-Global Instance from_always_absolutely_filter_spatial `{BiAffine PROP} P :
-  FromAlways always_modality_absolutely_filter_spatial (∀ᵢ P) P | 0.
-Proof. by rewrite /FromAlways. Qed.
+Global Instance from_modal_absolutely P :
+  FromModal modality_absolutely (∀ᵢ P) P | 1.
+Proof. by rewrite /FromModal. Qed.
+Global Instance from_modal_relatively P :
+  FromModal modality_id (∃ᵢ P) P | 1.
+Proof. by rewrite /FromModal /= -monPred_relatively_intro. Qed.
 
 Global Instance make_monPred_at_pure φ i : MakeMonPredAt i ⌜φ⌝ ⌜φ⌝.
 Proof. by rewrite /MakeMonPredAt monPred_at_pure. Qed.
@@ -168,23 +158,23 @@ Proof.
   by rewrite -monPred_at_persistently -monPred_at_persistently_if.
 Qed.
 
-Global Instance from_always_affinely_monPred_at P Q 𝓠 i :
-  FromAlways always_modality_affinely P Q → MakeMonPredAt i Q 𝓠 →
-  FromAlways always_modality_affinely (P i) 𝓠 | 0.
+Global Instance from_modal_affinely_monPred_at P Q 𝓠 i :
+  FromModal modality_affinely P Q → MakeMonPredAt i Q 𝓠 →
+  FromModal modality_affinely (P i) 𝓠 | 0.
 Proof.
-  rewrite /FromAlways /MakeMonPredAt /==> <- <-. by rewrite monPred_at_affinely.
+  rewrite /FromModal /MakeMonPredAt /==> <- <-. by rewrite monPred_at_affinely.
 Qed.
-Global Instance from_always_persistently_monPred_at P Q 𝓠 i :
-  FromAlways always_modality_persistently P Q → MakeMonPredAt i Q 𝓠 →
-  FromAlways always_modality_persistently (P i) 𝓠 | 0.
+Global Instance from_modal_persistently_monPred_at P Q 𝓠 i :
+  FromModal modality_persistently P Q → MakeMonPredAt i Q 𝓠 →
+  FromModal modality_persistently (P i) 𝓠 | 0.
 Proof.
-  rewrite /FromAlways /MakeMonPredAt /==> <- <-. by rewrite monPred_at_persistently.
+  rewrite /FromModal /MakeMonPredAt /==> <- <-. by rewrite monPred_at_persistently.
 Qed.
-Global Instance from_always_affinely_persistently_monPred_at P Q 𝓠 i :
-  FromAlways always_modality_affinely_persistently P Q → MakeMonPredAt i Q 𝓠 →
-  FromAlways always_modality_affinely_persistently (P i) 𝓠 | 0.
+Global Instance from_modal_affinely_persistently_monPred_at P Q 𝓠 i :
+  FromModal modality_affinely_persistently P Q → MakeMonPredAt i Q 𝓠 →
+  FromModal modality_affinely_persistently (P i) 𝓠 | 0.
 Proof.
-  rewrite /FromAlways /MakeMonPredAt /==> <- <-.
+  rewrite /FromModal /MakeMonPredAt /==> <- <-.
   by rewrite monPred_at_affinely monPred_at_persistently.
 Qed.
 
@@ -363,9 +353,11 @@ Proof.
 Qed.
 
 Global Instance from_modal_monPred_at i P Q 𝓠 :
-  FromModal P Q → MakeMonPredAt i Q 𝓠 → FromModal (P i) 𝓠.
+  FromModal modality_id P Q → MakeMonPredAt i Q 𝓠 → FromModal modality_id (P i) 𝓠.
 Proof. by rewrite /FromModal /MakeMonPredAt=> <- <-. Qed.
-
+Global Instance into_embed_absolute P :
+  Absolute P → IntoEmbed P (∀ i, P i).
+Proof. rewrite /IntoEmbed=> ?. by rewrite {1}(absolute_absolutely P). Qed.
 End bi.
 
 (* When P and/or Q are evars when doing typeclass search on [IntoWand
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index f7c535f5bbe636331c03574cfcf792d765ac4dc7..c50c6dbd85d7114a304455dee26bb56873731de1 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -961,50 +961,35 @@ Local Tactic Notation "iExistDestruct" constr(H)
     [env_reflexivity || fail "iExistDestruct:" Hx "not fresh"
     |revert y; intros x].
 
-(** * Always *)
-Tactic Notation "iAlways":=
+(** * Modality introduction *)
+Tactic Notation "iModIntro" open_constr(M) :=
   iStartProof;
-  eapply tac_always_intro;
+  eapply tac_modal_intro with M _ _ _ _;
     [apply _  ||
-     fail "iAlways: the goal is not an always-style modality"
-    |hnf; env_cbv; apply _ ||
-     lazymatch goal with
-     | |- TCAnd (TCForall ?C _) _ => fail "iAlways: persistent context does not satisfy" C
-     | |- TCAnd (TCEq _ Enil) _ => fail "iAlways: persistent context is non-empty"
+     fail "iModIntro: the goal is not a modality"
+    |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; apply _ ||
-     lazymatch goal with
-     | |- TCAnd (TCForall ?C _) _ => fail "iAlways: spatial context does not satisfy" C
-     | |- TCAnd (TCEq _ Enil) _ => fail "iAlways: spatial 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: 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 "iModIntro" := iModIntro _.
+Tactic Notation "iAlways" := iModIntro.
 
 (** * Later *)
-Tactic Notation "iNext" open_constr(n) :=
-  iStartProof;
-  let P := match goal with |- envs_entails _ ?P => P end in
-  try lazymatch n with 0 => fail 1 "iNext: cannot strip 0 laters" end;
-  (* apply is sometimes confused wrt. canonical structures search.
-     refine should use the other unification algorithm, which should
-     not have this issue. *)
-  notypeclasses refine (tac_next _ _ n _ _ _ _ _);
-    [apply _ || fail "iNext:" P "does not contain" n "laters"
-    |lazymatch goal with
-     | |- MaybeIntoLaterNEnvs 0 _ _ => fail "iNext:" P "does not contain laters"
-     | _ => apply _
-     end
-    |lazy beta (* remove beta redexes caused by removing laters under binders*)].
-
-Tactic Notation "iNext":= iNext _.
+Tactic Notation "iNext" open_constr(n) := iModIntro (modality_laterN n).
+Tactic Notation "iNext" := iModIntro (modality_laterN _).
 
 (** * Update modality *)
-Tactic Notation "iModIntro" :=
-  iStartProof;
-  eapply tac_modal_intro;
-    [apply _ ||
-     let P := match goal with |- FromModal ?P _ => P end in
-     fail "iModIntro:" P "not a modality"|].
-
 Tactic Notation "iModCore" constr(H) :=
   eapply tac_modal_elim with _ H _ _ _ _ _;
     [env_reflexivity || fail "iMod:" H "not found"
diff --git a/theories/tests/proofmode_monpred.v b/theories/tests/proofmode_monpred.v
index 3b2d68c24326ec552498991ec4e9d6471f1334be..af40b762f84c0d373fbae6aff9689be6fa746491 100644
--- a/theories/tests/proofmode_monpred.v
+++ b/theories/tests/proofmode_monpred.v
@@ -7,6 +7,7 @@ Section tests.
   Local Notation monPredI := (monPredI I PROP).
   Local Notation monPredSI := (monPredSI I PROP).
   Implicit Types P Q R : monPred.
+  Implicit Types 𝓟 𝓠 𝓡 : PROP.
   Implicit Types i j : I.
 
   Lemma test0 P : P -∗ P.
@@ -71,10 +72,22 @@ Section tests.
   Lemma test_absolutely P Q : ∀ᵢ emp -∗ ∀ᵢ P -∗ ∀ᵢ Q -∗ ∀ᵢ (P ∗ Q).
   Proof. iIntros "#? HP HQ". iAlways. by iSplitL "HP". Qed.
 
-  Lemma test_absolutely_affine `{BiAffine PROP} P Q R :
+  Lemma test_absolutely_absorbing P Q R `{!Absorbing P} :
     ∀ᵢ emp -∗ ∀ᵢ P -∗ ∀ᵢ Q -∗ R -∗ ∀ᵢ (P ∗ Q).
   Proof. iIntros "#? HP HQ HR". iAlways. by iSplitL "HP". Qed.
 
+  Lemma test_absolutely_affine P Q R `{!Affine R} :
+    ∀ᵢ emp -∗ ∀ᵢ P -∗ ∀ᵢ Q -∗ R -∗ ∀ᵢ (P ∗ Q).
+  Proof. iIntros "#? HP HQ HR". iAlways. by iSplitL "HP". Qed.
+
+  Lemma test_iModIntro_embed P `{!Affine Q} 𝓟 𝓠 :
+    □ P -∗ Q -∗ ⎡𝓟⎤ -∗ ⎡𝓠⎤ -∗ ⎡ 𝓟 ∗ 𝓠 ⎤.
+  Proof. iIntros "#H1 _ H2 H3". iAlways. iFrame. Qed.
+
+  Lemma test_iModIntro_embed_absolute P `{!Absolute Q} 𝓟 𝓠 :
+    □ P -∗ Q -∗ ⎡𝓟⎤ -∗ ⎡𝓠⎤ -∗ ⎡ ∀ i, 𝓟 ∗ 𝓠 ∗ Q i ⎤.
+  Proof. iIntros "#H1 H2 H3 H4". iAlways. iFrame. Qed.
+
   (* This is a hack to avoid avoid coq bug #5735: sections variables
      ignore hint modes. So we assume the instances in a way that
      cannot be used by type class resolution, and then declare the