diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 745fd6013a47f59042da695487b48049636f9ec3..ac5e9cf57c10ad06210c29ba7a38745369ee3c2a 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -383,6 +383,18 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   default emp mP
   
+1 goal
+  
+  PROP : bi
+  H : BiAffine PROP
+  P, Q : PROP
+  H0 : Laterable Q
+  ============================
+  "HP" : â–· P
+  "HQ" : Q
+  --------------------------------------∗
+  ▷ P ∗ Q
+  
 "elim_mod_accessor"
      : string
 1 goal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 454da8ec78f183803c0c52ad445b845eb3884553..afcfd89f24e1c9f6aa25391448e8fe50fe7e6c51 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,3 +1,4 @@
+From iris.bi Require Import laterable.
 From iris.proofmode Require Import tactics intro_patterns.
 Set Default Proof Using "Type".
 
@@ -1079,6 +1080,13 @@ Proof.
   iIntros "[P _]". done.
 Qed.
 
+Lemma test_iModIntro_make_laterable `{BiAffine PROP} (P Q : PROP) :
+  Laterable Q →
+  P -∗ Q -∗ make_laterable (▷ P ∗ Q).
+Proof.
+  iIntros (?) "HP HQ". iModIntro. Show. by iFrame.
+Qed.
+
 End tests.
 
 Section parsing_tests.