diff --git a/tests/atomic.ref b/tests/atomic.ref
index de749e7a9a6a7afdb81bfd57462e6394de21b03e..0c7d1674c490a6b94777c96bcd2e76c136a1d8ad 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -1,3 +1,5 @@
+The command has indeed failed with message:
+Tactic failure: iAuIntro: spacial context empty, and emp not laterable.
 1 goal
   
   Σ : gFunctors
diff --git a/tests/atomic.v b/tests/atomic.v
index 20b83453ae78bb5247f22ff82974d7dc9c1afdcf..8fa7ac6fd3937b46b0229a0c937c03ebf69a8884 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -6,7 +6,7 @@ From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
-Section definition.
+Section general_bi_tests.
   Context `{BiFUpd PROP} {TA TB : tele} (Eo Ei : coPset).
 
   (** We can quantify over telescopes *inside* Iris and use them with atomic
@@ -14,7 +14,17 @@ Section definition.
   Definition AU_tele_quantify_iris : Prop :=
     ⊢ ∀ (TA TB : tele) (α : TA → PROP) (β Φ : TA → TB → PROP),
         atomic_update Eo Ei α β Φ.
-End definition.
+
+  (** iAuIntro works with non-empty laterable spacial context without any further
+  assumptions. *)
+  Lemma au_intro_1 (P : PROP) `{!Laterable P} (α : TA → PROP) (β Φ : TA → TB → PROP) :
+    P -∗ atomic_update Eo Ei α β Φ.
+  Proof. iIntros "HP". iAuIntro. Abort.
+  (** But in an empty context, it fails, since [emp] now needs to be laterable. *)
+  Lemma au_intro_2 (α : TA → PROP) (β Φ : TA → TB → PROP) :
+    ⊢ atomic_update Eo Ei α β Φ.
+  Proof. Fail iAuIntro. Abort.
+End general_bi_tests.
 
 Section tests.
   Context `{!heapGS Σ} {aheap: atomic_heap Σ}.