diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 636692cadcd90d3b2c2ba83d8e073298c350718c..691d79dbecdc6d5033dcc5588a480738709c45c9 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -932,6 +932,13 @@ Global Instance into_laterN_exist {A} n (Φ Ψ : A → PROP) :
   IntoLaterN' n (∃ x, Φ x) (∃ x, Ψ x).
 Proof. rewrite /IntoLaterN' /IntoLaterN -laterN_exist_2=> ?. by apply exist_mono. Qed.
 
+Global Instance into_later_bare n P Q :
+  IntoLaterN n P Q → IntoLaterN n (■ P) (■ Q).
+Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_bare_2. Qed.
+Global Instance into_later_persistently n P Q :
+  IntoLaterN n P Q → IntoLaterN n (□ P) (□ Q).
+Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_persistently. Qed.
+
 Global Instance into_laterN_sep_l n P1 P2 Q1 Q2 :
   IntoLaterN' n P1 Q1 → IntoLaterN n P2 Q2 →
   IntoLaterN' n (P1 ∗ P2) (Q1 ∗ Q2) | 10.
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 07a5175f1deca724aa73f66c95a2436272facf75..e57ccad6b96f1c93c03b2b24df380aaef32a0d92 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -217,6 +217,11 @@ Lemma test_iIntros_let P :
   ∀ Q, let R := emp%I in P -∗ R -∗ Q -∗ P ∗ Q.
 Proof. iIntros (Q R) "$ _ $". Qed.
 
+Lemma test_foo P Q : ■ ▷ (Q ≡ P) -∗ ■ ▷ Q -∗ ■ ▷ P.
+Proof.
+  iIntros "#HPQ HQ". iSplit; first done. iNext. by iRewrite "HPQ" in "HQ".
+Qed.
+
 Lemma test_iIntros_modalities `(!Absorbing P) :
   (□ ▷ ∀  x : nat, ⌜ x = 0 ⌝ → ⌜ x = 0 ⌝ -∗ False -∗ P -∗ P)%I.
 Proof.
@@ -224,4 +229,5 @@ Proof.
   iIntros "* **". (* Test that fast intros do not work under modalities *)
   iIntros ([]).
 Qed.
+
 End tests.