diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 817edd512e3e8d298906736c73e56f0807af7a0c..9557c72f6e21f9b842188df0f5a0a969bfda67f6 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -435,13 +435,6 @@ Proof.
 Qed.
 
 (** * Basic rules *)
-Lemma tac_emp_intro Δ :
-  env_spatial_is_nil Δ = true →
-  Δ ⊢ emp.
-Proof.
-  intros. by rewrite (env_spatial_is_nil_bare_persistently Δ) // (affine (⬕ Δ)).
-Qed.
-
 Class AffineEnv (Γ : env PROP) := affine_env : Forall Affine Γ.
 Global Instance affine_env_nil : AffineEnv Enil.
 Proof. constructor. Qed.
@@ -453,6 +446,14 @@ Instance affine_env_spatial Δ :
   TCOr (AffineBI PROP) (AffineEnv (env_spatial Δ)) → Affine ([∗] env_spatial Δ).
 Proof. destruct 1 as [?|H]. apply _. induction H; simpl; apply _. Qed.
 
+Lemma tac_emp_intro Δ :
+  (* Establishing [AffineEnv (env_spatial Δ)] is rather expensive (linear in the
+  size of the context), so first check whether the whole BI is affine (which
+  takes constant time). *)
+  TCOr (AffineBI PROP) (AffineEnv (env_spatial Δ)) →
+  Δ ⊢ emp.
+Proof. intros [?|?]; by rewrite (affine Δ). Qed.
+
 Lemma tac_assumption Δ Δ' i p P Q :
   envs_lookup_delete i Δ = Some (p,P,Δ') →
   FromAssumption p P Q →
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 51eb5eabd7d114497d4bd28ddcc4cc40a4d766b8..b9b48ab08b580f1c281dde694f12187ea5364d48 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -202,7 +202,8 @@ Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
 Tactic Notation "iEmpIntro" :=
   iStartProof;
   eapply tac_emp_intro;
-    [env_reflexivity || fail "iEmpIntro: spatial context is non-empty"].
+    [env_cbv; apply _ ||
+     fail "iEmpIntro: spatial context contains non-affine hypotheses"].
 
 Tactic Notation "iPureIntro" :=
   iStartProof;
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 7aaec057ba3dd55f4867dca5d47efd83386c026e..8c6ce8060c557808b0d822767a70bde85fc8082b 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -91,6 +91,10 @@ Lemma test_iSpecialize_auto_frame P Q R :
   (P -∗ True -∗ True -∗ Q -∗ R) -∗ P -∗ Q -∗ R.
 Proof. iIntros "H HP HQ". by iApply ("H" with "[$]"). Qed.
 
+Lemma test_iEmp_intro P Q R `{!Affine P, !Persistent Q, !Affine R} :
+  P -∗ Q → R -∗ emp.
+Proof. iIntros "HP #HQ HR". iEmpIntro. Qed.
+
 (* Check coercions *)
 Lemma test_iExist_coercion (P : Z → PROP) : (∀ x, P x) -∗ ∃ x, P x.
 Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.