diff --git a/ProofMode.md b/ProofMode.md
index 7d8bd9b15e381ec3f8c7a36709c895d843da29a6..acc6d86defda6fd245e5da7953f4f36d543ad85f 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -114,15 +114,15 @@ Separating logic specific tactics
 Modalities
 ----------
 
-- `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,
+- `iModIntro mod` : 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.
+  The optional argument `mod` can be used to specify what modality to introduce
+  in case of ambiguity, e.g. `⎡|==> P⎤`.
 - `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`.
+- `iNext n` : an alias of `iModIntro (â–·^n P)`.
+- `iNext` : an alias of `iModIntro (â–·^1 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.
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 561c1a24a6927e0f266ff3f5ebb735903455cddf..4fe308424257bf7b870f7091073562b357f8ff20 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -127,7 +127,7 @@ Lemma slice_delete_empty E q f P Q γ :
   ↑N ⊆ E →
   f !! γ = Some false →
   slice N γ Q -∗ ▷?q box N f P ={E}=∗ ∃ P',
-    ▷?q ▷ (P ≡ (Q ∗ P')) ∗ ▷?q box N (delete γ f) P'.
+    ▷?q (▷ (P ≡ (Q ∗ P')) ∗ box N (delete γ f) P').
 Proof.
   iIntros (??) "[#HγQ Hinv] H". iDestruct "H" as (Φ) "[#HeqP Hf]".
   iExists ([∗ map] γ'↦_ ∈ delete γ f, Φ γ')%I.
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 42744be61acee5c14dae305ccb92dd5a669030cc..6235d121511b3ab21a1d910d6502aac828ae9614 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -57,7 +57,7 @@ Section proofs.
     ▷ □ (P ↔ P') -∗ cinv N γ P -∗ cinv N γ P'.
   Proof.
     iIntros "#HP' Hinv". iDestruct "Hinv" as (P'') "[#HP'' Hinv]".
-    iExists _. iFrame "Hinv". iNext. iAlways. iSplit.
+    iExists _. iFrame "Hinv". iAlways. iNext. iSplit.
     - iIntros "?". iApply "HP''". iApply "HP'". done.
     - iIntros "?". iApply "HP'". iApply "HP''". done.
   Qed.
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 0521d09d7a9610fd3933d74ea78dea91a9e8ca6e..a16239aaa8362cbc61a549a52a26c32a10559ef5 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -107,7 +107,7 @@ Implicit Types σ : state.
 
 (** Base axioms for core primitives of the language: Stateless reductions *)
 Lemma wp_fork s E e Φ :
-  ▷ Φ (LitV LitUnit) ∗ ▷ WP e @ s; ⊤ {{ _, True }} ⊢ WP Fork e @ s; E {{ Φ }}.
+  ▷ (Φ (LitV LitUnit) ∗ WP e @ s; ⊤ {{ _, True }}) ⊢ WP Fork e @ s; E {{ Φ }}.
 Proof.
   iIntros "[HΦ He]".
   iApply wp_lift_pure_det_head_step; [auto|intros; inv_head_step; eauto|].
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index ece99f113359585fb1f3ab7909a4a538db08a397..65ec13c6fc6ce20756abea1527b53a572c27ca8b 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -1394,12 +1394,12 @@ 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 n P Q :
-  NoBackTrack (FromLaterN n P Q) →
-  TCIf (TCEq n 0) False TCTrue →
-  FromModal (modality_laterN n) (â–·^n P) P Q | 99.
-  (* below [from_modal_embed] to prefer introducing a later *)
-Proof. rewrite /FromLaterN /FromModal. by intros [?] [_ []|?]. Qed.
+Global Instance from_modal_later P :
+  FromModal (modality_laterN 1) (â–·^1 P) (â–· P) P.
+Proof. by rewrite /FromModal. Qed.
+Global Instance from_modal_laterN n P :
+  FromModal (modality_laterN n) (â–·^n P) (â–·^n P) P.
+Proof. by rewrite /FromModal. Qed.
 Global Instance from_modal_except_0 P : FromModal modality_id (â—‡ P) (â—‡ P) P.
 Proof. by rewrite /FromModal /= -except_0_intro. Qed.
 
@@ -1681,55 +1681,4 @@ Proof.
   rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
   rewrite big_opMS_commute. by apply big_sepMS_mono.
 Qed.
-
-(* FromLater *)
-Global Instance from_laterN_later P : FromLaterN 1 (â–· P) P | 0.
-Proof. by rewrite /FromLaterN. Qed.
-Global Instance from_laterN_laterN n P : FromLaterN n (â–·^n P) P | 0.
-Proof. by rewrite /FromLaterN. Qed.
-
-(* The instances below are used when stripping a specific number of laters, or
-to balance laters in different branches of ∧, ∨ and ∗. *)
-Global Instance from_laterN_0 P : FromLaterN 0 P P | 100. (* fallthrough *)
-Proof. by rewrite /FromLaterN. Qed.
-Global Instance from_laterN_later_S n P Q :
-  FromLaterN n P Q → FromLaterN (S n) (▷ P) Q.
-Proof. by rewrite /FromLaterN=><-. Qed.
-Global Instance from_laterN_later_plus n m P Q :
-  FromLaterN m P Q → FromLaterN (n + m) (▷^n P) Q.
-Proof. rewrite /FromLaterN=><-. by rewrite laterN_plus. Qed.
-
-Global Instance from_later_and n P1 P2 Q1 Q2 :
-  FromLaterN n P1 Q1 → FromLaterN n P2 Q2 → FromLaterN n (P1 ∧ P2) (Q1 ∧ Q2).
-Proof. intros ??; red. by rewrite laterN_and; apply and_mono. Qed.
-Global Instance from_later_or n P1 P2 Q1 Q2 :
-  FromLaterN n P1 Q1 → FromLaterN n P2 Q2 → FromLaterN n (P1 ∨ P2) (Q1 ∨ Q2).
-Proof. intros ??; red. by rewrite laterN_or; apply or_mono. Qed.
-Global Instance from_later_sep n P1 P2 Q1 Q2 :
-  FromLaterN n P1 Q1 → FromLaterN n P2 Q2 → FromLaterN n (P1 ∗ P2) (Q1 ∗ Q2).
-Proof. intros ??; red. by rewrite laterN_sep; apply sep_mono. Qed.
-
-Global Instance from_later_affinely n P Q `{BiAffine PROP} :
-  FromLaterN n P Q → FromLaterN n (bi_affinely P) (bi_affinely Q).
-Proof. rewrite /FromLaterN=><-. by rewrite affinely_elim affine_affinely. Qed.
-Global Instance from_later_plainly n P Q :
-  FromLaterN n P Q → FromLaterN n (bi_plainly P) (bi_plainly Q).
-Proof. by rewrite /FromLaterN laterN_plainly=> ->. Qed.
-Global Instance from_later_persistently n P Q :
-  FromLaterN n P Q → FromLaterN n (bi_persistently P) (bi_persistently Q).
-Proof. by rewrite /FromLaterN laterN_persistently=> ->. Qed.
-Global Instance from_later_absorbingly n P Q :
-  FromLaterN n P Q → FromLaterN n (bi_absorbingly P) (bi_absorbingly Q).
-Proof. by rewrite /FromLaterN laterN_absorbingly=> ->. Qed.
-Global Instance from_later_embed`{SbiEmbedding PROP PROP'} n P Q :
-  FromLaterN n P Q → FromLaterN n ⎡P⎤ ⎡Q⎤.
-Proof. rewrite /FromLaterN=> <-. by rewrite sbi_embed_laterN. Qed.
-
-Global Instance from_later_forall {A} n (Φ Ψ : A → PROP) :
-  (∀ x, FromLaterN n (Φ x) (Ψ x)) → FromLaterN n (∀ x, Φ x) (∀ x, Ψ x).
-Proof. rewrite /FromLaterN laterN_forall=> ?. by apply forall_mono. Qed.
-Global Instance from_later_exist {A} n (Φ Ψ : A → PROP) :
-  Inhabited A → (∀ x, FromLaterN n (Φ x) (Ψ x)) →
-  FromLaterN n (∃ x, Φ x) (∃ x, Ψ x).
-Proof. intros ?. rewrite /FromLaterN laterN_exist=> ?. by apply exist_mono. Qed.
 End sbi_instances.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 04ae2c701d5f8f513723f0f80c3ba145c05fdfb8..5786a01a7b83abacdeef05ec58eeaab2234ac439 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -446,11 +446,6 @@ Instance maybe_into_laterN_default_0 {PROP : sbi} only_head (P : PROP) :
   MaybeIntoLaterN only_head 0 P P | 0.
 Proof. apply _. Qed.
 
-Class FromLaterN {PROP : sbi} (n : nat) (P Q : PROP) := from_laterN : ▷^n Q ⊢ P.
-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].
 
@@ -531,8 +526,6 @@ Instance into_pure_tc_opaque {PROP : bi} (P : PROP) φ :
   IntoPure P φ → IntoPure (tc_opaque P) φ := id.
 Instance from_pure_tc_opaque {PROP : bi} (a : bool) (P : PROP) φ :
   FromPure a P φ → FromPure a (tc_opaque P) φ := id.
-Instance from_laterN_tc_opaque {PROP : sbi} n (P Q : PROP) :
-  FromLaterN n P Q → FromLaterN n (tc_opaque P) Q := id.
 Instance from_wand_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
   FromWand P Q1 Q2 → FromWand (tc_opaque P) Q1 Q2 := id.
 Instance into_wand_tc_opaque {PROP : bi} p q (R P Q : PROP) :
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index d89bfb20c0aa0cdeea72e21edb15e71529154c2f..d60a2635dab284e36feb439b4d75d49e25c1229b 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -430,12 +430,13 @@ Global Instance maybe_into_later_monPred_at i n P Q 𝓠 :
   IntoLaterN false n (P i) 𝓠.
 Proof.
   rewrite /IntoLaterN /MaybeIntoLaterN /MakeMonPredAt=> -> <-. elim n=>//= ? <-.
-   by rewrite monPred_at_later.
+  by rewrite monPred_at_later.
 Qed.
-Global Instance from_later_monPred_at i n P Q 𝓠 :
-  FromLaterN n P Q → MakeMonPredAt i Q 𝓠 → FromLaterN n (P i) 𝓠.
+Global Instance from_later_monPred_at i `(sel : A) n P Q 𝓠 :
+  FromModal (modality_laterN n) sel P Q → MakeMonPredAt i Q 𝓠 →
+  FromModal (modality_laterN n) sel (P i) 𝓠.
 Proof.
-  rewrite /FromLaterN /MakeMonPredAt=> <- <-. elim n=>//= ? ->.
+  rewrite /FromModal /MakeMonPredAt=> <- <-. elim n=>//= ? ->.
   by rewrite monPred_at_later.
 Qed.
 
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index d97463a4beeeb9b434e79b939998952496ede29e..53589bbd4d41cce95ca6eeee1453c1b73029fb64 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -171,9 +171,8 @@ Proof.
   iIntros "?". iNext. iAssumption.
 Qed.
 
-Lemma test_iNext_sep1 P Q
-    (R1 := (P ∗ Q)%I) (R2 := (▷ P ∗ ▷ Q)%I) :
-  (▷ P ∗ ▷ Q) ∗ R1 ∗ R2 -∗ ▷ (P ∗ Q) ∗ ▷ R1 ∗ R2.
+Lemma test_iNext_sep1 P Q (R1 := (P ∗ Q)%I) :
+  (▷ P ∗ ▷ Q) ∗ R1 -∗ ▷ ((P ∗ Q) ∗ R1).
 Proof.
   iIntros "H". iNext.
   rewrite {1 2}(lock R1). (* check whether R1 has not been unfolded *) done.