diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 94025c311a3cb5bdc5661a17fbc33fa06b05d4fb..2b65b88c7d2d736a7d60b52d142c86e17e0acbdf 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -127,7 +127,7 @@ Proof.
   iSpecialize ("HΦ" with "[#]") => //. iFrame "HΦ".
   iMod ("Hclose" $! (State High I) (∅ : set token) with "[-]"); last done.
   iSplit; [iPureIntro; by eauto using signal_step|].
-  iNext. rewrite {2}/barrier_inv /ress /=; iFrame "Hl".
+  rewrite {2}/barrier_inv /ress /=. iNext. iFrame "Hl".
   iDestruct "Hr" as (Ψ) "[Hr Hsp]"; iExists Ψ; iFrame "Hsp".
   iNext. iIntros "_"; by iApply "Hr".
 Qed.
@@ -142,7 +142,7 @@ Proof.
     as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
   wp_load. destruct p.
   - iMod ("Hclose" $! (State Low I) {[ Change i ]} with "[Hl Hr]") as "Hγ".
-    { iSplit; first done. iNext. rewrite {2}/barrier_inv /=. by iFrame. }
+    { iSplit; first done. rewrite {2}/barrier_inv /=. by iFrame. }
     iAssert (sts_ownS γ (i_states i) {[Change i]})%I with ">[Hγ]" as "Hγ".
     { iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
     iModIntro. wp_if.
@@ -155,7 +155,7 @@ Proof.
     { iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". }
     iMod ("Hclose" $! (State High (I ∖ {[ i ]})) (∅ : set token) with "[HΨ' Hl Hsp]").
     { iSplit; [iPureIntro; by eauto using wait_step|].
-      iNext. rewrite {2}/barrier_inv /=; iFrame "Hl". iExists Ψ; iFrame. auto. }
+      rewrite {2}/barrier_inv /=. iNext. iFrame "Hl". iExists Ψ; iFrame. auto. }
     iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by auto.
     iModIntro. wp_if.
     iApply "HΦ". iApply "HQR". by iRewrite "Heq".
@@ -175,7 +175,7 @@ Proof.
   iMod ("Hclose" $! (State p ({[i1; i2]} ∪ I ∖ {[i]}))
                    {[Change i1; Change i2 ]} with "[-]") as "Hγ".
   { iSplit; first by eauto using split_step.
-    iNext. rewrite {2}/barrier_inv /=. iFrame "Hl".
+    rewrite {2}/barrier_inv /=. iNext. iFrame "Hl".
     iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame; auto. }
   iAssert (sts_ownS γ (i_states i1) {[Change i1]}
     ∗ sts_ownS γ (i_states i2) {[Change i2]})%I with ">[-]" as "[Hγ1 Hγ2]".
diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index 060133dd55a22df57253ba2ec3cc25922852b366..309f2095bb27845de67368a79efd787755913fb8 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -15,7 +15,7 @@ Implicit Types Δ : envs (iResUR Σ).
 Lemma tac_wp_alloc Δ Δ' E j e v Φ :
   to_val e = Some v →
   (Δ ⊢ heap_ctx) → ↑heapN ⊆ E →
-  IntoLaterEnvs Δ Δ' →
+  IntoLaterNEnvs 1 Δ Δ' →
   (∀ l, ∃ Δ'',
     envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧
     (Δ'' ⊢ Φ (LitV (LitLoc l)))) →
@@ -23,28 +23,28 @@ Lemma tac_wp_alloc Δ Δ' E j e v Φ :
 Proof.
   intros ???? HΔ. eapply wand_apply; first exact:wp_alloc. rewrite -always_and_sep_l.
   apply and_intro; first done.
-  rewrite into_later_env_sound; apply later_mono, forall_intro=> l.
+  rewrite into_laterN_env_sound; apply later_mono, forall_intro=> l.
   destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
   by rewrite right_id HΔ'.
 Qed.
 
 Lemma tac_wp_load Δ Δ' E i l q v Φ :
   (Δ ⊢ heap_ctx) → ↑heapN ⊆ E →
-  IntoLaterEnvs Δ Δ' →
+  IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
   (Δ' ⊢ Φ v) →
   Δ ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
 Proof.
   intros. eapply wand_apply; first exact:wp_load. rewrite -assoc -always_and_sep_l.
   apply and_intro; first done.
-  rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
+  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
 Lemma tac_wp_store Δ Δ' Δ'' E i l v e v' Φ :
   to_val e = Some v' →
   (Δ ⊢ heap_ctx) → ↑heapN ⊆ E →
-  IntoLaterEnvs Δ Δ' →
+  IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
   (Δ'' ⊢ Φ (LitV LitUnit)) →
@@ -52,28 +52,28 @@ Lemma tac_wp_store Δ Δ' Δ'' E i l v e v' Φ :
 Proof.
   intros. eapply wand_apply; first by eapply wp_store. rewrite -assoc -always_and_sep_l.
   apply and_intro; first done.
-  rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
+  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
 Lemma tac_wp_cas_fail Δ Δ' E i l q v e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
   (Δ ⊢ heap_ctx) → ↑heapN ⊆ E →
-  IntoLaterEnvs Δ Δ' →
+  IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 →
   (Δ' ⊢ Φ (LitV (LitBool false))) →
   Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
   intros. eapply wand_apply; first exact:wp_cas_fail. rewrite -assoc -always_and_sep_l.
   apply and_intro; first done.
-  rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
+  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
 Lemma tac_wp_cas_suc Δ Δ' Δ'' E i l v e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
   (Δ ⊢ heap_ctx) → ↑heapN ⊆ E →
-  IntoLaterEnvs Δ Δ' →
+  IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I → v = v1 →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
   (Δ'' ⊢ Φ (LitV (LitBool true))) →
@@ -81,7 +81,7 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' E i l v e1 v1 e2 v2 Φ :
 Proof.
   intros; subst. eapply wand_apply; first exact:wp_cas_suc. rewrite -assoc -always_and_sep_l.
   apply and_intro; first done.
-  rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
+  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 End heap.
diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index 741ac556e9e2043dffe2501ceff0a437108d9c2d..6730918d20dd51ed2a6184e3b0c0403409e44679 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -1,5 +1,6 @@
 From iris.proofmode Require Export classes.
 From iris.algebra Require Import gmap.
+From iris.prelude Require Import gmultiset.
 From iris.base_logic Require Import big_op.
 Import uPred.
 
@@ -58,47 +59,81 @@ Global Instance into_persistentP_persistent P :
 Proof. done. Qed.
 
 (* IntoLater *)
-Global Instance into_later_default P : IntoLater P P | 1000.
-Proof. apply later_intro. Qed.
-Global Instance into_later_later P : IntoLater (â–· P) P.
+Global Instance into_laterN_default n P : IntoLaterN n P P | 1000.
+Proof. apply laterN_intro. Qed.
+Global Instance into_laterN_later n P Q :
+  IntoLaterN n P Q → IntoLaterN (S n) (▷ P) Q.
+Proof. by rewrite /IntoLaterN=>->. Qed.
+Global Instance into_laterN_laterN n P : IntoLaterN n (â–·^n P) P.
 Proof. done. Qed.
-Global Instance into_later_and P1 P2 Q1 Q2 :
-  IntoLater P1 Q1 → IntoLater P2 Q2 → IntoLater (P1 ∧ P2) (Q1 ∧ Q2).
-Proof. intros ??; red. by rewrite later_and; apply and_mono. Qed.
-Global Instance into_later_or P1 P2 Q1 Q2 :
-  IntoLater P1 Q1 → IntoLater P2 Q2 → IntoLater (P1 ∨ P2) (Q1 ∨ Q2).
-Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed.
-Global Instance into_later_sep P1 P2 Q1 Q2 :
-  IntoLater P1 Q1 → IntoLater P2 Q2 → IntoLater (P1 ∗ P2) (Q1 ∗ Q2).
-Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.
-
-Global Instance into_later_big_sepM `{Countable K} {A}
+Global Instance into_laterN_laterN_plus n m P Q :
+  IntoLaterN m P Q → IntoLaterN (n + m) (▷^n P) Q.
+Proof. rewrite /IntoLaterN=>->. by rewrite laterN_plus. Qed.
+
+Global Instance into_laterN_and n P1 P2 Q1 Q2 :
+  IntoLaterN n P1 Q1 → IntoLaterN n P2 Q2 → IntoLaterN n (P1 ∧ P2) (Q1 ∧ Q2).
+Proof. intros ??; red. by rewrite laterN_and; apply and_mono. Qed.
+Global Instance into_laterN_or n P1 P2 Q1 Q2 :
+  IntoLaterN n P1 Q1 → IntoLaterN n P2 Q2 → IntoLaterN n (P1 ∨ P2) (Q1 ∨ Q2).
+Proof. intros ??; red. by rewrite laterN_or; apply or_mono. Qed.
+Global Instance into_laterN_sep n P1 P2 Q1 Q2 :
+  IntoLaterN n P1 Q1 → IntoLaterN n P2 Q2 → IntoLaterN n (P1 ∗ P2) (Q1 ∗ Q2).
+Proof. intros ??; red. by rewrite laterN_sep; apply sep_mono. Qed.
+
+Global Instance into_laterN_big_sepL n {A} (Φ Ψ : nat → A → uPred M) (l: list A) :
+  (∀ x k, IntoLaterN n (Φ k x) (Ψ k x)) →
+  IntoLaterN n ([∗ list] k ↦ x ∈ l, Φ k x) ([∗ list] k ↦ x ∈ l, Ψ k x).
+Proof.
+  rewrite /IntoLaterN=> ?. rewrite big_sepL_laterN. by apply big_sepL_mono.
+Qed.
+Global Instance into_laterN_big_sepM n `{Countable K} {A}
     (Φ Ψ : K → A → uPred M) (m : gmap K A) :
-  (∀ x k, IntoLater (Φ k x) (Ψ k x)) →
-  IntoLater ([∗ map] k ↦ x ∈ m, Φ k x) ([∗ map] k ↦ x ∈ m, Ψ k x).
+  (∀ x k, IntoLaterN n (Φ k x) (Ψ k x)) →
+  IntoLaterN n ([∗ map] k ↦ x ∈ m, Φ k x) ([∗ map] k ↦ x ∈ m, Ψ k x).
 Proof.
-  rewrite /IntoLater=> ?. rewrite big_sepM_later; by apply big_sepM_mono.
+  rewrite /IntoLaterN=> ?. rewrite big_sepM_laterN; by apply big_sepM_mono.
 Qed.
-Global Instance into_later_big_sepS `{Countable A}
+Global Instance into_laterN_big_sepS n `{Countable A}
     (Φ Ψ : A → uPred M) (X : gset A) :
-  (∀ x, IntoLater (Φ x) (Ψ x)) →
-  IntoLater ([∗ set] x ∈ X, Φ x) ([∗ set] x ∈ X, Ψ x).
+  (∀ x, IntoLaterN n (Φ x) (Ψ x)) →
+  IntoLaterN n ([∗ set] x ∈ X, Φ x) ([∗ set] x ∈ X, Ψ x).
+Proof.
+  rewrite /IntoLaterN=> ?. rewrite big_sepS_laterN; by apply big_sepS_mono.
+Qed.
+Global Instance into_laterN_big_sepMS n `{Countable A}
+    (Φ Ψ : A → uPred M) (X : gmultiset A) :
+  (∀ x, IntoLaterN n (Φ x) (Ψ x)) →
+  IntoLaterN n ([∗ mset] x ∈ X, Φ x) ([∗ mset] x ∈ X, Ψ x).
 Proof.
-  rewrite /IntoLater=> ?. rewrite big_sepS_later; by apply big_sepS_mono.
+  rewrite /IntoLaterN=> ?. rewrite big_sepMS_laterN; by apply big_sepMS_mono.
 Qed.
 
 (* FromLater *)
-Global Instance from_later_later P : FromLater (â–· P) P.
+Global Instance from_laterN_later P :FromLaterN 1 (â–· P) P | 0.
 Proof. done. Qed.
-Global Instance from_later_and P1 P2 Q1 Q2 :
-  FromLater P1 Q1 → FromLater P2 Q2 → FromLater (P1 ∧ P2) (Q1 ∧ Q2).
-Proof. intros ??; red. by rewrite later_and; apply and_mono. Qed.
-Global Instance from_later_or P1 P2 Q1 Q2 :
-  FromLater P1 Q1 → FromLater P2 Q2 → FromLater (P1 ∨ P2) (Q1 ∨ Q2).
-Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed.
-Global Instance from_later_sep P1 P2 Q1 Q2 :
-  FromLater P1 Q1 → FromLater P2 Q2 → FromLater (P1 ∗ P2) (Q1 ∗ Q2).
-Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.
+Global Instance from_laterN_laterN n P : FromLaterN n (â–·^n P) P | 0.
+Proof. done. 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. done. 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.
 
 (* IntoWand *)
 Global Instance into_wand_wand P Q Q' :
@@ -113,9 +148,12 @@ Global Instance into_wand_iff_r P Q : IntoWand (P ↔ Q) Q P.
 Proof. apply and_elim_r', impl_wand. Qed.
 Global Instance into_wand_always R P Q : IntoWand R P Q → IntoWand (□ R) P Q.
 Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
-Global Instance into_wand_later {M} (R P Q : uPred M) :
+Global Instance into_wand_later (R P Q : uPred M) :
   IntoWand R P Q → IntoWand R (▷ P) (▷ Q) | 100.
 Proof. rewrite /IntoWand=>->. by rewrite -later_wand -later_intro. Qed.
+Global Instance into_wand_laterN n (R P Q : uPred M) :
+  IntoWand R P Q → IntoWand R (▷^n P) (▷^n Q) | 100.
+Proof. rewrite /IntoWand=>->. by rewrite -laterN_wand -laterN_intro. Qed.
 Global Instance into_wand_bupd R P Q :
   IntoWand R P Q → IntoWand R (|==> P) (|==> Q) | 100.
 Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite bupd_wand_r. Qed.
@@ -137,6 +175,9 @@ Proof. rewrite /FromAnd=> <-. by rewrite always_and. Qed.
 Global Instance from_and_later P Q1 Q2 :
   FromAnd P Q1 Q2 → FromAnd (▷ P) (▷ Q1) (▷ Q2).
 Proof. rewrite /FromAnd=> <-. by rewrite later_and. Qed.
+Global Instance from_and_laterN n P Q1 Q2 :
+  FromAnd P Q1 Q2 → FromAnd (▷^n P) (▷^n Q1) (▷^n Q2).
+Proof. rewrite /FromAnd=> <-. by rewrite laterN_and. Qed.
 
 (* FromSep *)
 Global Instance from_sep_sep P1 P2 : FromSep (P1 ∗ P2) P1 P2 | 100.
@@ -153,23 +194,33 @@ Proof. rewrite /FromSep=> <-. by rewrite always_sep. Qed.
 Global Instance from_sep_later P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (▷ P) (▷ Q1) (▷ Q2).
 Proof. rewrite /FromSep=> <-. by rewrite later_sep. Qed.
+Global Instance from_sep_laterN n P Q1 Q2 :
+  FromSep P Q1 Q2 → FromSep (▷^n P) (▷^n Q1) (▷^n Q2).
+Proof. rewrite /FromSep=> <-. by rewrite laterN_sep. Qed.
 Global Instance from_sep_bupd P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (|==> P) (|==> Q1) (|==> Q2).
 Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
 
+Global Instance from_sep_big_sepL {A} (Φ Ψ1 Ψ2 : nat → A → uPred M) l :
+  (∀ k x, FromSep (Φ k x) (Ψ1 k x) (Ψ2 k x)) →
+  FromSep ([∗ list] k ↦ x ∈ l, Φ k x)
+    ([∗ list] k ↦ x ∈ l, Ψ1 k x) ([∗ list] k ↦ x ∈ l, Ψ2 k x).
+Proof. rewrite /FromSep=>?. rewrite -big_sepL_sepL. by apply big_sepL_mono. Qed.
 Global Instance from_sep_big_sepM
     `{Countable K} {A} (Φ Ψ1 Ψ2 : K → A → uPred M) m :
   (∀ k x, FromSep (Φ k x) (Ψ1 k x) (Ψ2 k x)) →
   FromSep ([∗ map] k ↦ x ∈ m, Φ k x)
     ([∗ map] k ↦ x ∈ m, Ψ1 k x) ([∗ map] k ↦ x ∈ m, Ψ2 k x).
-Proof.
-  rewrite /FromSep=> ?. rewrite -big_sepM_sepM. by apply big_sepM_mono.
-Qed.
+Proof. rewrite /FromSep=>?. rewrite -big_sepM_sepM. by apply big_sepM_mono. Qed.
 Global Instance from_sep_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A → uPred M) X :
   (∀ x, FromSep (Φ x) (Ψ1 x) (Ψ2 x)) →
   FromSep ([∗ set] x ∈ X, Φ x) ([∗ set] x ∈ X, Ψ1 x) ([∗ set] x ∈ X, Ψ2 x).
+Proof. rewrite /FromSep=>?. rewrite -big_sepS_sepS. by apply big_sepS_mono. Qed.
+Global Instance from_sep_big_sepMS `{Countable A} (Φ Ψ1 Ψ2 : A → uPred M) X :
+  (∀ x, FromSep (Φ x) (Ψ1 x) (Ψ2 x)) →
+  FromSep ([∗ mset] x ∈ X, Φ x) ([∗ mset] x ∈ X, Ψ1 x) ([∗ mset] x ∈ X, Ψ2 x).
 Proof.
-  rewrite /FromSep=> ?. rewrite -big_sepS_sepS. by apply big_sepS_mono.
+  rewrite /FromSep=> ?. rewrite -big_sepMS_sepMS. by apply big_sepMS_mono.
 Qed.
 
 (* FromOp *)
@@ -227,7 +278,19 @@ Qed.
 Global Instance into_and_later p P Q1 Q2 :
   IntoAnd p P Q1 Q2 → IntoAnd p (▷ P) (▷ Q1) (▷ Q2).
 Proof. rewrite /IntoAnd=>->. destruct p; by rewrite ?later_and ?later_sep. Qed.
+Global Instance into_and_laterN n p P Q1 Q2 :
+  IntoAnd p P Q1 Q2 → IntoAnd p (▷^n P) (▷^n Q1) (▷^n Q2).
+Proof. rewrite /IntoAnd=>->. destruct p; by rewrite ?laterN_and ?laterN_sep. Qed.
 
+Global Instance into_and_big_sepL {A} (Φ Ψ1 Ψ2 : nat → A → uPred M) p l :
+  (∀ k x, IntoAnd p (Φ k x) (Ψ1 k x) (Ψ2 k x)) →
+  IntoAnd p ([∗ list] k ↦ x ∈ l, Φ k x)
+    ([∗ list] k ↦ x ∈ l, Ψ1 k x) ([∗ list] k ↦ x ∈ l, Ψ2 k x).
+Proof.
+  rewrite /IntoAnd=> HΦ. destruct p.
+  - rewrite -big_sepL_and. apply big_sepL_mono; auto.
+  - rewrite -big_sepL_sepL. apply big_sepL_mono; auto.
+Qed.
 Global Instance into_and_big_sepM
     `{Countable K} {A} (Φ Ψ1 Ψ2 : K → A → uPred M) p m :
   (∀ k x, IntoAnd p (Φ k x) (Ψ1 k x) (Ψ2 k x)) →
@@ -235,9 +298,7 @@ Global Instance into_and_big_sepM
     ([∗ map] k ↦ x ∈ m, Ψ1 k x) ([∗ map] k ↦ x ∈ m, Ψ2 k x).
 Proof.
   rewrite /IntoAnd=> HΦ. destruct p.
-  - apply and_intro; apply big_sepM_mono; auto.
-    + intros k x ?. by rewrite HΦ and_elim_l.
-    + intros k x ?. by rewrite HΦ and_elim_r.
+  - rewrite -big_sepM_and. apply big_sepM_mono; auto.
   - rewrite -big_sepM_sepM. apply big_sepM_mono; auto.
 Qed.
 Global Instance into_and_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A → uPred M) p X :
@@ -245,11 +306,17 @@ Global Instance into_and_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A → uPred M) p
   IntoAnd p ([∗ set] x ∈ X, Φ x) ([∗ set] x ∈ X, Ψ1 x) ([∗ set] x ∈ X, Ψ2 x).
 Proof.
   rewrite /IntoAnd=> HΦ. destruct p.
-  - apply and_intro; apply big_sepS_mono; auto.
-    + intros x ?. by rewrite HΦ and_elim_l.
-    + intros x ?. by rewrite HΦ and_elim_r.
+  - rewrite -big_sepS_and. apply big_sepS_mono; auto.
   - rewrite -big_sepS_sepS. apply big_sepS_mono; auto.
 Qed.
+Global Instance into_and_big_sepMS `{Countable A} (Φ Ψ1 Ψ2 : A → uPred M) p X :
+  (∀ x, IntoAnd p (Φ x) (Ψ1 x) (Ψ2 x)) →
+  IntoAnd p ([∗ mset] x ∈ X, Φ x) ([∗ mset] x ∈ X, Ψ1 x) ([∗ mset] x ∈ X, Ψ2 x).
+Proof.
+  rewrite /IntoAnd=> HΦ. destruct p.
+  - rewrite -big_sepMS_and. apply big_sepMS_mono; auto.
+  - rewrite -big_sepMS_sepMS. apply big_sepMS_mono; auto.
+Qed.
 
 (* Frame *)
 Global Instance frame_here R : Frame R R True.
@@ -310,9 +377,21 @@ Global Instance make_later_default P : MakeLater P (â–· P) | 100.
 Proof. done. Qed.
 
 Global Instance frame_later R R' P Q Q' :
-  IntoLater R' R → Frame R P Q → MakeLater Q Q' → Frame R' (▷ P) Q'.
+  IntoLaterN 1 R' R → Frame R P Q → MakeLater Q Q' → Frame R' (▷ P) Q'.
 Proof.
-  rewrite /Frame /MakeLater /IntoLater=>-> <- <-. by rewrite later_sep.
+  rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-. by rewrite later_sep.
+Qed.
+
+Class MakeLaterN (n : nat) (P lP : uPred M) := make_laterN : ▷^n P ⊣⊢ lP.
+Global Instance make_laterN_true n : MakeLaterN n True True.
+Proof. by rewrite /MakeLaterN laterN_True. Qed.
+Global Instance make_laterN_default P : MakeLaterN n P (â–·^n P) | 100.
+Proof. done. Qed.
+
+Global Instance frame_laterN n R R' P Q Q' :
+  IntoLaterN n R' R → Frame R P Q → MakeLaterN n Q Q' → Frame R' (▷^n P) Q'.
+Proof.
+  rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-. by rewrite laterN_sep.
 Qed.
 
 Class MakeExcept0 (P Q : uPred M) := make_except_0 : ◇ P ⊣⊢ Q.
@@ -352,6 +431,9 @@ Proof. rewrite /FromOr=> <-. by rewrite always_or. Qed.
 Global Instance from_or_later P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (▷ P) (▷ Q1) (▷ Q2).
 Proof. rewrite /FromOr=><-. by rewrite later_or. Qed.
+Global Instance from_or_laterN n P Q1 Q2 :
+  FromOr P Q1 Q2 → FromOr (▷^n P) (▷^n Q1) (▷^n Q2).
+Proof. rewrite /FromOr=><-. by rewrite laterN_or. Qed.
 
 (* IntoOr *)
 Global Instance into_or_or P Q : IntoOr (P ∨ Q) P Q.
@@ -364,6 +446,9 @@ Proof. rewrite /IntoOr=>->. by rewrite always_or. Qed.
 Global Instance into_or_later P Q1 Q2 :
   IntoOr P Q1 Q2 → IntoOr (▷ P) (▷ Q1) (▷ Q2).
 Proof. rewrite /IntoOr=>->. by rewrite later_or. Qed.
+Global Instance into_or_laterN n P Q1 Q2 :
+  IntoOr P Q1 Q2 → IntoOr (▷^n P) (▷^n Q1) (▷^n Q2).
+Proof. rewrite /IntoOr=>->. by rewrite laterN_or. Qed.
 
 (* FromExist *)
 Global Instance from_exist_exist {A} (Φ : A → uPred M): FromExist (∃ a, Φ a) Φ.
@@ -386,6 +471,11 @@ Global Instance from_exist_later {A} P (Φ : A → uPred M) :
 Proof.
   rewrite /FromExist=> <-. apply exist_elim=>x. apply later_mono, exist_intro.
 Qed.
+Global Instance from_exist_laterN {A} n P (Φ : A → uPred M) :
+  FromExist P Φ → FromExist (▷^n P) (λ a, ▷^n (Φ a))%I.
+Proof.
+  rewrite /FromExist=> <-. apply exist_elim=>x. apply laterN_mono, exist_intro.
+Qed.
 
 (* IntoExist *)
 Global Instance into_exist_exist {A} (Φ : A → uPred M) : IntoExist (∃ a, Φ a) Φ.
@@ -393,12 +483,15 @@ Proof. done. Qed.
 Global Instance into_exist_pure {A} (φ : A → Prop) :
   @IntoExist M A ⌜∃ x, φ x⌝ (λ a, ⌜φ a⌝)%I.
 Proof. by rewrite /IntoExist pure_exist. Qed.
-Global Instance into_exist_later {A} P (Φ : A → uPred M) :
-  IntoExist P Φ → Inhabited A → IntoExist (▷ P) (λ a, ▷ (Φ a))%I.
-Proof. rewrite /IntoExist=> HP ?. by rewrite HP later_exist. Qed.
 Global Instance into_exist_always {A} P (Φ : A → uPred M) :
   IntoExist P Φ → IntoExist (□ P) (λ a, □ (Φ a))%I.
 Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed.
+Global Instance into_exist_later {A} P (Φ : A → uPred M) :
+  IntoExist P Φ → Inhabited A → IntoExist (▷ P) (λ a, ▷ (Φ a))%I.
+Proof. rewrite /IntoExist=> HP ?. by rewrite HP later_exist. Qed.
+Global Instance into_exist_laterN {A} n P (Φ : A → uPred M) :
+  IntoExist P Φ → Inhabited A → IntoExist (▷^n P) (λ a, ▷^n (Φ a))%I.
+Proof. rewrite /IntoExist=> HP ?. by rewrite HP laterN_exist. Qed.
 
 (* IntoModal *)
 Global Instance into_modal_later P : IntoModal P (â–· P).
@@ -438,6 +531,12 @@ Proof.
   intros. rewrite /ElimModal (except_0_intro (_ -∗ _)) (timelessP P).
   by rewrite -except_0_sep wand_elim_r.
 Qed.
+Global Instance elim_modal_timeless_bupd' p P Q :
+  TimelessP P → IsExcept0 Q → ElimModal (▷?p P) P Q Q.
+Proof.
+  destruct p; simpl; auto using elim_modal_timeless_bupd.
+  intros _ _. by rewrite /ElimModal wand_elim_r.
+Qed.
 
 Global Instance is_except_0_except_0 P : IsExcept0 (â—‡ P).
 Proof. by rewrite /IsExcept0 except_0_idemp. Qed.
diff --git a/proofmode/classes.v b/proofmode/classes.v
index c9b0bccb9cc92daaf86fcf07ba838d5edf7e527b..ed2689753698f7c0888ac1c0cbf81f2ae3822b8e 100644
--- a/proofmode/classes.v
+++ b/proofmode/classes.v
@@ -17,11 +17,11 @@ Global Arguments from_pure : clear implicits.
 Class IntoPersistentP (P Q : uPred M) := into_persistentP : P ⊢ □ Q.
 Global Arguments into_persistentP : clear implicits.
 
-Class IntoLater (P Q : uPred M) := into_later : P ⊢ ▷ Q.
-Global Arguments into_later _ _ {_}.
+Class IntoLaterN (n : nat) (P Q : uPred M) := into_laterN : P ⊢ ▷^n Q.
+Global Arguments into_laterN _ _ _ {_}.
 
-Class FromLater (P Q : uPred M) := from_later : ▷ Q ⊢ P.
-Global Arguments from_later _ _ {_}.
+Class FromLaterN (n : nat) (P Q : uPred M) := from_laterN : ▷^n Q ⊢ P.
+Global Arguments from_laterN _ _ _ {_}.
 
 Class IntoWand (R P Q : uPred M) := into_wand : R ⊢ P -∗ Q.
 Global Arguments into_wand : clear implicits.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index f741bd26be26d33d4d1facacb3ba151828262889..c51703240d1ad5f930d9057b466d829cf3eecbb1 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -401,38 +401,38 @@ Lemma tac_pure_revert Δ φ Q : (Δ ⊢ ⌜φ⌝ → Q) → (φ → Δ ⊢ Q).
 Proof. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
 
 (** * Later *)
-Class IntoLaterEnv (Γ1 Γ2 : env (uPred M)) :=
-  into_later_env : env_Forall2 IntoLater Γ1 Γ2.
-Class IntoLaterEnvs (Δ1 Δ2 : envs M) := {
-  into_later_persistent: IntoLaterEnv (env_persistent Δ1) (env_persistent Δ2);
-  into_later_spatial: IntoLaterEnv (env_spatial Δ1) (env_spatial Δ2)
+Class IntoLaterNEnv (n : nat) (Γ1 Γ2 : env (uPred M)) :=
+  into_laterN_env : env_Forall2 (IntoLaterN n) Γ1 Γ2.
+Class IntoLaterNEnvs (n : nat) (Δ1 Δ2 : envs M) := {
+  into_later_persistent: IntoLaterNEnv n (env_persistent Δ1) (env_persistent Δ2);
+  into_later_spatial: IntoLaterNEnv n (env_spatial Δ1) (env_spatial Δ2)
 }.
 
-Global Instance into_later_env_nil : IntoLaterEnv Enil Enil.
+Global Instance into_laterN_env_nil n : IntoLaterNEnv n Enil Enil.
 Proof. constructor. Qed.
-Global Instance into_later_env_snoc Γ1 Γ2 i P Q :
-  IntoLaterEnv Γ1 Γ2 → IntoLater P Q →
-  IntoLaterEnv (Esnoc Γ1 i P) (Esnoc Γ2 i Q).
+Global Instance into_laterN_env_snoc n Γ1 Γ2 i P Q :
+  IntoLaterNEnv n Γ1 Γ2 → IntoLaterN n P Q →
+  IntoLaterNEnv n (Esnoc Γ1 i P) (Esnoc Γ2 i Q).
 Proof. by constructor. Qed.
 
-Global Instance into_later_envs Γp1 Γp2 Γs1 Γs2 :
-  IntoLaterEnv Γp1 Γp2 → IntoLaterEnv Γs1 Γs2 →
-  IntoLaterEnvs (Envs Γp1 Γs1) (Envs Γp2 Γs2).
+Global Instance into_laterN_envs n Γp1 Γp2 Γs1 Γs2 :
+  IntoLaterNEnv n Γp1 Γp2 → IntoLaterNEnv n Γs1 Γs2 →
+  IntoLaterNEnvs n (Envs Γp1 Γs1) (Envs Γp2 Γs2).
 Proof. by split. Qed.
 
-Lemma into_later_env_sound Δ1 Δ2 : IntoLaterEnvs Δ1 Δ2 → Δ1 ⊢ ▷ Δ2.
+Lemma into_laterN_env_sound n Δ1 Δ2 : IntoLaterNEnvs n Δ1 Δ2 → Δ1 ⊢ ▷^n Δ2.
 Proof.
-  intros [Hp Hs]; rewrite /of_envs /= !later_sep -always_later.
+  intros [Hp Hs]; rewrite /of_envs /= !laterN_sep -always_laterN.
   repeat apply sep_mono; try apply always_mono.
-  - rewrite -later_intro; apply pure_mono; destruct 1; constructor;
+  - rewrite -laterN_intro; apply pure_mono; destruct 1; constructor;
       naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
-  - induction Hp; rewrite /= ?later_sep. apply later_intro. by apply sep_mono.
-  - induction Hs; rewrite /= ?later_sep. apply later_intro. by apply sep_mono.
+  - induction Hp; rewrite /= ?laterN_sep. apply laterN_intro. by apply sep_mono.
+  - induction Hs; rewrite /= ?laterN_sep. apply laterN_intro. by apply sep_mono.
 Qed.
 
-Lemma tac_next Δ Δ' Q Q' :
-  IntoLaterEnvs Δ Δ' → FromLater Q Q' → (Δ' ⊢ Q') → Δ ⊢ Q.
-Proof. intros ?? HQ. by rewrite -(from_later Q) into_later_env_sound HQ. Qed.
+Lemma tac_next Δ Δ' n Q Q' :
+  FromLaterN n Q Q' → IntoLaterNEnvs n Δ Δ' → (Δ' ⊢ Q') → Δ ⊢ Q.
+Proof. intros ?? HQ. by rewrite -(from_laterN n Q) into_laterN_env_sound HQ. Qed.
 
 Lemma tac_löb Δ Δ' i Q :
   env_spatial_is_nil Δ = true →
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index ae871b9505f6237015be7f350caff1d9a47452cb..f1dec70d91212dd6a3e325d23d9c8ac8014ab05b 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -608,11 +608,17 @@ Tactic Notation "iAlways":=
     [reflexivity || fail "iAlways: spatial context non-empty"|].
 
 (** * Later *)
-Tactic Notation "iNext":=
-  eapply tac_next;
-    [apply _
-    |let P := match goal with |- FromLater ?P _ => P end in
-     apply _ || fail "iNext:" P "does not contain laters"|].
+Tactic Notation "iNext" open_constr(n) :=
+  let P := match goal with |- _ ⊢ ?P => P end in
+  try lazymatch n with 0 => fail 1 "iNext: cannot strip 0 laters" end;
+  eapply (tac_next _ _ n);
+    [apply _ || fail "iNext:" P "does not contain" n "laters"
+    |lazymatch goal with
+     | |- IntoLaterNEnvs 0 _ _ => fail "iNext:" P "does not contain laters"
+     | _ => apply _
+     end|].
+
+Tactic Notation "iNext":= iNext _.
 
 (** * Update modality *)
 Tactic Notation "iModIntro" :=