diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index f473b0b39f03ccdcb3bd5e2248b50835d5ac623b..e69e3827ffbb6bd8f62f4b73c20b7f5d761cc0b5 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -1092,8 +1092,6 @@ Global Instance from_modal_embed `{BiEmbedding PROP PROP'} P Q :
   FromModal P Q â†’ FromModal âŽ¡PâŽ¤ âŽ¡QâŽ¤.
 Proof. by rewrite /FromModal=> ->. Qed.
 
-(* ElimModal *)
-
 (* AsValid *)
 Global Instance as_valid_valid {PROP : bi} (P : PROP) : AsValid0 (bi_valid P) P | 0.
 Proof. by rewrite /AsValid. Qed.
@@ -1550,14 +1548,14 @@ Global Instance make_laterN_default P : MakeLaterN n P (â–·^n P) | 100.
 Proof. by rewrite /MakeLaterN. Qed.
 
 Global Instance frame_later p R R' P Q Q' :
-  NoBackTrack (MaybeIntoLaterN 1 R' R) â†’
+  NoBackTrack (MaybeIntoLaterN true 1 R' R) â†’
   Frame p R P Q â†’ MakeLaterN 1 Q Q' â†’ Frame p R' (â–· P) Q'.
 Proof.
   rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
   by rewrite later_affinely_persistently_if_2 later_sep.
 Qed.
 Global Instance frame_laterN p n R R' P Q Q' :
-  NoBackTrack (MaybeIntoLaterN n R' R) â†’
+  NoBackTrack (MaybeIntoLaterN true n R' R) â†’
   Frame p R P Q â†’ MakeLaterN n Q Q' â†’ Frame p R' (â–·^n P) Q'.
 Proof.
   rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
@@ -1587,116 +1585,121 @@ Proof.
 Qed.
 
 (* IntoLater *)
-Global Instance into_laterN_0 P : IntoLaterN 0 P P.
+Global Instance into_laterN_0 only_head P : IntoLaterN only_head 0 P P.
 Proof. by rewrite /IntoLaterN /MaybeIntoLaterN. Qed.
-Global Instance into_laterN_later n n' m' P Q lQ :
+Global Instance into_laterN_later only_head n n' m' P Q lQ :
   NatCancel n 1 n' m' â†’
   (** If canceling has failed (i.e. [1 = m']), we should make progress deeper
   into [P], as such, we continue with the [IntoLaterN] class, which is required
   to make progress. If canceling has succeeded, we do not need to make further
   progress, but there may still be a left-over (i.e. [n']) to cancel more deeply
   into [P], as such, we continue with [MaybeIntoLaterN]. *)
-  TCIf (TCEq 1 m') (IntoLaterN n' P Q) (MaybeIntoLaterN n' P Q) â†’
+  TCIf (TCEq 1 m') (IntoLaterN only_head n' P Q) (MaybeIntoLaterN only_head n' P Q) â†’
   MakeLaterN m' Q lQ â†’
-  IntoLaterN n (â–· P) lQ | 2.
+  IntoLaterN only_head n (â–· P) lQ | 2.
 Proof.
   rewrite /MakeLaterN /IntoLaterN /MaybeIntoLaterN /NatCancel.
   move=> Hn [_ ->|->] <-;
     by rewrite -later_laterN -laterN_plus -Hn Nat.add_comm.
 Qed.
-Global Instance into_laterN_laterN n m n' m' P Q lQ :
+Global Instance into_laterN_laterN only_head n m n' m' P Q lQ :
   NatCancel n m n' m' â†’
-  TCIf (TCEq m m') (IntoLaterN n' P Q) (MaybeIntoLaterN n' P Q) â†’
+  TCIf (TCEq m m') (IntoLaterN only_head n' P Q) (MaybeIntoLaterN only_head n' P Q) â†’
   MakeLaterN m' Q lQ â†’
-  IntoLaterN n (â–·^m P) lQ | 1.
+  IntoLaterN only_head n (â–·^m P) lQ | 1.
 Proof.
   rewrite /MakeLaterN /IntoLaterN /MaybeIntoLaterN /NatCancel.
   move=> Hn [_ ->|->] <-; by rewrite -!laterN_plus -Hn Nat.add_comm.
 Qed.
 
 Global Instance into_laterN_and_l n P1 P2 Q1 Q2 :
-  IntoLaterN n P1 Q1 â†’ MaybeIntoLaterN n P2 Q2 â†’
-  IntoLaterN n (P1 âˆ§ P2) (Q1 âˆ§ Q2) | 10.
+  IntoLaterN false n P1 Q1 â†’ MaybeIntoLaterN false n P2 Q2 â†’
+  IntoLaterN false n (P1 âˆ§ P2) (Q1 âˆ§ Q2) | 10.
 Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> -> ->. by rewrite laterN_and. Qed.
 Global Instance into_laterN_and_r n P P2 Q2 :
-  IntoLaterN n P2 Q2 â†’ IntoLaterN n (P âˆ§ P2) (P âˆ§ Q2) | 11.
+  IntoLaterN false n P2 Q2 â†’ IntoLaterN false n (P âˆ§ P2) (P âˆ§ Q2) | 11.
 Proof.
   rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_and -(laterN_intro _ P).
 Qed.
 
+Global Instance into_laterN_forall {A} n (Î¦ Î¨ : A â†’ PROP) :
+  (âˆ€ x, IntoLaterN false n (Î¦ x) (Î¨ x)) â†’
+  IntoLaterN false n (âˆ€ x, Î¦ x) (âˆ€ x, Î¨ x).
+Proof. rewrite /IntoLaterN /MaybeIntoLaterN laterN_forall=> ?. by apply forall_mono. Qed.
+Global Instance into_laterN_exist {A} n (Î¦ Î¨ : A â†’ PROP) :
+  (âˆ€ x, IntoLaterN false n (Î¦ x) (Î¨ x)) â†’
+  IntoLaterN false n (âˆƒ x, Î¦ x) (âˆƒ x, Î¨ x).
+Proof. rewrite /IntoLaterN /MaybeIntoLaterN -laterN_exist_2=> ?. by apply exist_mono. Qed.
+
 Global Instance into_laterN_or_l n P1 P2 Q1 Q2 :
-  IntoLaterN n P1 Q1 â†’ MaybeIntoLaterN n P2 Q2 â†’
-  IntoLaterN n (P1 âˆ¨ P2) (Q1 âˆ¨ Q2) | 10.
+  IntoLaterN false n P1 Q1 â†’ MaybeIntoLaterN false n P2 Q2 â†’
+  IntoLaterN false n (P1 âˆ¨ P2) (Q1 âˆ¨ Q2) | 10.
 Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> -> ->. by rewrite laterN_or. Qed.
 Global Instance into_laterN_or_r n P P2 Q2 :
-  IntoLaterN n P2 Q2 â†’
-  IntoLaterN n (P âˆ¨ P2) (P âˆ¨ Q2) | 11.
+  IntoLaterN false n P2 Q2 â†’
+  IntoLaterN false n (P âˆ¨ P2) (P âˆ¨ Q2) | 11.
 Proof.
   rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_or -(laterN_intro _ P).
 Qed.
 
-Global Instance into_laterN_forall {A} n (Î¦ Î¨ : A â†’ PROP) :
-  (âˆ€ x, IntoLaterN n (Î¦ x) (Î¨ x)) â†’ IntoLaterN n (âˆ€ x, Î¦ x) (âˆ€ x, Î¨ x).
-Proof. rewrite /IntoLaterN /MaybeIntoLaterN laterN_forall=> ?. by apply forall_mono. Qed.
-Global Instance into_laterN_exist {A} n (Î¦ Î¨ : A â†’ PROP) :
-  (âˆ€ x, IntoLaterN n (Î¦ x) (Î¨ x)) â†’
-  IntoLaterN n (âˆƒ x, Î¦ x) (âˆƒ x, Î¨ x).
-Proof. rewrite /IntoLaterN /MaybeIntoLaterN -laterN_exist_2=> ?. by apply exist_mono. Qed.
-
 Global Instance into_later_affinely n P Q :
-  MaybeIntoLaterN n P Q â†’ MaybeIntoLaterN n (bi_affinely P) (bi_affinely Q).
+  MaybeIntoLaterN false n P Q â†’
+  MaybeIntoLaterN false n (bi_affinely P) (bi_affinely Q).
 Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite laterN_affinely_2. Qed.
 Global Instance into_later_absorbingly n P Q :
-  MaybeIntoLaterN n P Q â†’ MaybeIntoLaterN n (bi_absorbingly P) (bi_absorbingly Q).
+  MaybeIntoLaterN false n P Q â†’
+  MaybeIntoLaterN false n (bi_absorbingly P) (bi_absorbingly Q).
 Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite laterN_absorbingly. Qed.
 Global Instance into_later_plainly n P Q :
-  MaybeIntoLaterN n P Q â†’ MaybeIntoLaterN n (bi_plainly P) (bi_plainly Q).
+  MaybeIntoLaterN false n P Q â†’
+  MaybeIntoLaterN false n (bi_plainly P) (bi_plainly Q).
 Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite laterN_plainly. Qed.
 Global Instance into_later_persistently n P Q :
-  MaybeIntoLaterN n P Q â†’ MaybeIntoLaterN n (bi_persistently P) (bi_persistently Q).
+  MaybeIntoLaterN false n P Q â†’
+  MaybeIntoLaterN false n (bi_persistently P) (bi_persistently Q).
 Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite laterN_persistently. Qed.
 Global Instance into_later_embed`{SbiEmbedding PROP PROP'} n P Q :
-  MaybeIntoLaterN n P Q â†’ MaybeIntoLaterN n âŽ¡PâŽ¤ âŽ¡QâŽ¤.
+  MaybeIntoLaterN false n P Q â†’ MaybeIntoLaterN false n âŽ¡PâŽ¤ âŽ¡QâŽ¤.
 Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite sbi_embed_laterN. Qed.
 
 Global Instance into_laterN_sep_l n P1 P2 Q1 Q2 :
-  IntoLaterN n P1 Q1 â†’ MaybeIntoLaterN n P2 Q2 â†’
-  IntoLaterN n (P1 âˆ— P2) (Q1 âˆ— Q2) | 10.
+  IntoLaterN false n P1 Q1 â†’ MaybeIntoLaterN false n P2 Q2 â†’
+  IntoLaterN false n (P1 âˆ— P2) (Q1 âˆ— Q2) | 10.
 Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> -> ->. by rewrite laterN_sep. Qed.
 Global Instance into_laterN_sep_r n P P2 Q2 :
-  IntoLaterN n P2 Q2 â†’
-  IntoLaterN n (P âˆ— P2) (P âˆ— Q2) | 11.
+  IntoLaterN false n P2 Q2 â†’
+  IntoLaterN false n (P âˆ— P2) (P âˆ— Q2) | 11.
 Proof.
   rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_sep -(laterN_intro _ P).
 Qed.
 
 Global Instance into_laterN_big_sepL n {A} (Î¦ Î¨ : nat â†’ A â†’ PROP) (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).
+  (âˆ€ x k, IntoLaterN false n (Î¦ k x) (Î¨ k x)) â†’
+  IntoLaterN false n ([âˆ— list] k â†¦ x âˆˆ l, Î¦ k x) ([âˆ— list] k â†¦ x âˆˆ l, Î¨ k x).
 Proof.
   rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
   rewrite big_opL_commute. by apply big_sepL_mono.
 Qed.
 Global Instance into_laterN_big_sepM n `{Countable K} {A}
     (Î¦ Î¨ : K â†’ A â†’ PROP) (m : gmap K A) :
-  (âˆ€ x k, IntoLaterN n (Î¦ k x) (Î¨ k x)) â†’
-  IntoLaterN n ([âˆ— map] k â†¦ x âˆˆ m, Î¦ k x) ([âˆ— map] k â†¦ x âˆˆ m, Î¨ k x).
+  (âˆ€ x k, IntoLaterN false n (Î¦ k x) (Î¨ k x)) â†’
+  IntoLaterN false n ([âˆ— map] k â†¦ x âˆˆ m, Î¦ k x) ([âˆ— map] k â†¦ x âˆˆ m, Î¨ k x).
 Proof.
   rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
   rewrite big_opM_commute. by apply big_sepM_mono.
 Qed.
 Global Instance into_laterN_big_sepS n `{Countable A}
     (Î¦ Î¨ : A â†’ PROP) (X : gset A) :
-  (âˆ€ x, IntoLaterN n (Î¦ x) (Î¨ x)) â†’
-  IntoLaterN n ([âˆ— set] x âˆˆ X, Î¦ x) ([âˆ— set] x âˆˆ X, Î¨ x).
+  (âˆ€ x, IntoLaterN false n (Î¦ x) (Î¨ x)) â†’
+  IntoLaterN false n ([âˆ— set] x âˆˆ X, Î¦ x) ([âˆ— set] x âˆˆ X, Î¨ x).
 Proof.
   rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
   rewrite big_opS_commute. by apply big_sepS_mono.
 Qed.
 Global Instance into_laterN_big_sepMS n `{Countable A}
     (Î¦ Î¨ : A â†’ PROP) (X : gmultiset A) :
-  (âˆ€ x, IntoLaterN n (Î¦ x) (Î¨ x)) â†’
-  IntoLaterN n ([âˆ— mset] x âˆˆ X, Î¦ x) ([âˆ— mset] x âˆˆ X, Î¨ x).
+  (âˆ€ x, IntoLaterN false n (Î¦ x) (Î¨ x)) â†’
+  IntoLaterN false n ([âˆ— mset] x âˆˆ X, Î¦ x) ([âˆ— mset] x âˆˆ X, Î¨ x).
 Proof.
   rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
   rewrite big_opMS_commute. by apply big_sepMS_mono.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index c8f8629023eccc606a8d65d1f7fe91f50986c48a..796a4c3a5e4b23cca131050514ca49bea8c47b35 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -239,6 +239,7 @@ Converting an assumption [R] into a wand [P -âˆ— Q] is done in three stages:
   hypothesis).
 - Instantiate the premise of the wand or implication.
 *)
+
 Class IntoWand {PROP : bi} (p q : bool) (R P Q : PROP) :=
   into_wand : â–¡?p R âŠ¢ â–¡?q P -âˆ— Q.
 Arguments IntoWand {_} _ _ _%I _%I _%I : simpl never.
@@ -416,26 +417,36 @@ IntoLaterN n P P'       MaybeIntoLaterN n Q Q'
 -------------------------------
 IntoLaterN n (P /\ Q) (P /\ Q')
 >>
+
+The Boolean [only_head] indicates whether laters should only be stripped in
+head position or also below other logical connectives. For [iNext] it should
+strip laters below other logical connectives, but this should not happen while
+framing, e.g. the following should succeed:
+
+<<
+Lemma test_iFrame_later_1 P Q : P âˆ— â–· Q -âˆ— â–· (P âˆ— â–· Q).
+Proof. iIntros "H". iFrame "H". Qed.
+>>
 *)
-Class MaybeIntoLaterN {PROP : sbi} (n : nat) (P Q : PROP) :=
+Class MaybeIntoLaterN {PROP : sbi} (only_head : bool) (n : nat) (P Q : PROP) :=
   maybe_into_laterN : P âŠ¢ â–·^n Q.
-Arguments MaybeIntoLaterN {_} _%nat_scope _%I _%I.
-Arguments maybe_into_laterN {_} _%nat_scope _%I _%I {_}.
-Hint Mode MaybeIntoLaterN + - - - : typeclass_instances.
+Arguments MaybeIntoLaterN {_} _ _%nat_scope _%I _%I.
+Arguments maybe_into_laterN {_} _ _%nat_scope _%I _%I {_}.
+Hint Mode MaybeIntoLaterN + + + - - : typeclass_instances.
 
-Class IntoLaterN {PROP : sbi} (n : nat) (P Q : PROP) :=
-  into_laterN :> MaybeIntoLaterN n P Q.
-Arguments IntoLaterN {_} _%nat_scope _%I _%I.
-Hint Mode IntoLaterN + - ! - : typeclass_instances.
+Class IntoLaterN {PROP : sbi} (only_head : bool) (n : nat) (P Q : PROP) :=
+  into_laterN :> MaybeIntoLaterN only_head n P Q.
+Arguments IntoLaterN {_} _ _%nat_scope _%I _%I.
+Hint Mode IntoLaterN + + + ! - : typeclass_instances.
 
-Instance maybe_into_laterN_default {PROP : sbi} n (P : PROP) :
-  MaybeIntoLaterN n P P | 1000.
+Instance maybe_into_laterN_default {PROP : sbi} only_head n (P : PROP) :
+  MaybeIntoLaterN only_head n P P | 1000.
 Proof. apply laterN_intro. Qed.
 (* In the case both parameters are evars and n=0, we have to stop the
    search and unify both evars immediately instead of looping using
    other instances. *)
-Instance maybe_into_laterN_default_0 {PROP : sbi} (P : PROP) :
-  MaybeIntoLaterN 0 P P | 0.
+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.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index a34a4aab169efa7a7a62d05518874d6bd4a40d6c..33c0287b721cc75bc8f38bfe3dc75915af4d2f5b 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -1206,16 +1206,16 @@ Qed.
 
 (** * Later *)
 Class MaybeIntoLaterNEnv (n : nat) (Î“1 Î“2 : env PROP) :=
-  into_laterN_env : env_Forall2 (MaybeIntoLaterN n) Î“1 Î“2.
+  into_laterN_env : env_Forall2 (MaybeIntoLaterN false n) Î“1 Î“2.
 Class MaybeIntoLaterNEnvs (n : nat) (Î”1 Î”2 : envs PROP) := {
-  into_later_persistent: MaybeIntoLaterNEnv n (env_persistent Î”1) (env_persistent Î”2);
+  into_later_persistent:  MaybeIntoLaterNEnv n (env_persistent Î”1) (env_persistent Î”2);
   into_later_spatial: MaybeIntoLaterNEnv n (env_spatial Î”1) (env_spatial Î”2)
 }.
 
 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 n 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.
 
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 0b4165240dea1a17d050f8ae9d6a885a3b85a3fa..ae5a975dc089cc9b3a38037ff2257d87fae0457b 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -433,7 +433,8 @@ Global Instance into_except_0_monPred_at_bwd i P ð“Ÿ Q :
 Proof. rewrite /IntoExcept0 /MakeMonPredAt=> H <-. by rewrite H monPred_at_except_0. Qed.
 
 Global Instance maybe_into_later_monPred_at i n P Q ð“  :
-  MaybeIntoLaterN n P Q â†’ MakeMonPredAt i Q ð“  â†’ MaybeIntoLaterN n (P i) ð“ .
+  MaybeIntoLaterN false n P Q â†’ MakeMonPredAt i Q ð“  â†’
+  MaybeIntoLaterN false n (P i) ð“ .
 Proof.
   rewrite /MaybeIntoLaterN /MakeMonPredAt=> -> <-. elim n=>//= ? <-.
    by rewrite monPred_at_later.
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 040a0a430833f14d13da41d2e4853aa234bd2b52..aaef16cd02a3347ea28ca9b6ebc50aae0dec6838 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -356,4 +356,10 @@ Proof.
   iEval (rewrite (Nat.add_comm x y) // H).
   done.
 Qed.
+
+Lemma test_iFrame_later_1 P Q : P âˆ— â–· Q -âˆ— â–· (P âˆ— â–· Q).
+Proof. iIntros "H". iFrame "H". auto. Qed.
+
+Lemma test_iFrame_later_2 P Q : â–· P âˆ— â–· Q -âˆ— â–· (â–· P âˆ— â–· Q).
+Proof. iIntros "H". iFrame "H". auto. Qed.
 End tests.