diff --git a/tests/proofmode.v b/tests/proofmode.v
index 4443bbb9df7ce6788d3bdf8c5f75d0fd8785c12d..197fed735db30bd25ed9297b007774f832c288d7 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -158,6 +158,9 @@ Lemma test_iFrame_conjunction_2 P Q :
   P -∗ Q -∗ (P ∧ P) ∗ (Q ∧ Q).
 Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
 
+Lemma test_iFrame_later `{BiAffine PROP} P Q : P -∗ Q -∗ ▷ P ∗ Q.
+Proof. iIntros "H1 H2". by iFrame "H1". Qed.
+
 Lemma test_iAssert_modality P : ◇ False -∗ ▷ P.
 Proof.
   iIntros "HF".
diff --git a/theories/proofmode/frame_instances.v b/theories/proofmode/frame_instances.v
index 387608462e5f3c803b7473b8b0769490978adfad..b382f7f90262f902bac00b8bb2703acef70d7004 100644
--- a/theories/proofmode/frame_instances.v
+++ b/theories/proofmode/frame_instances.v
@@ -270,6 +270,9 @@ Proof. rewrite /Frame /MakeEmbed -embed_internal_eq. apply (frame_embed p P Q).
 
 Global Instance make_laterN_true n : @KnownMakeLaterN PROP n True True | 0.
 Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_True. Qed.
+Global Instance make_laterN_emp `{!BiAffine PROP} n :
+  @KnownMakeLaterN PROP n emp emp | 0.
+Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_emp. Qed.
 Global Instance make_laterN_0 P : MakeLaterN 0 P P | 0.
 Proof. by rewrite /MakeLaterN. Qed.
 Global Instance make_laterN_1 P : MakeLaterN 1 P (â–· P) | 2.