diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index e273f9f45298a96afb684008dbe0331a8e525d1d..9e971ae75af93bdc0b1857c9fbd711614f62b407 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -524,8 +524,14 @@ Proof.
 Qed.
 
 (** * Pure *)
-Lemma tac_pure_intro Δ Q φ : FromPure false Q φ → φ → envs_entails Δ Q.
-Proof. intros ??. rewrite envs_entails_eq -(from_pure _ Q). by apply pure_intro. Qed.
+Lemma tac_pure_intro Δ Q φ af :
+  env_spatial_is_nil Δ = af → FromPure af Q φ → φ → envs_entails Δ Q.
+Proof.
+  intros ???. rewrite envs_entails_eq -(from_pure _ Q). destruct af.
+  - rewrite env_spatial_is_nil_affinely_persistently //=. f_equiv.
+    by apply pure_intro.
+  - by apply pure_intro.
+Qed.
 
 Lemma tac_pure Δ Δ' i p P φ Q :
   envs_lookup_delete i Δ = Some (p, P, Δ') →
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index 2e5abfb3162b9411d54928a67153d6d2bc6509d9..4816f938a0daae36ba3b2bcd964b00bb3936b3a9 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -69,12 +69,6 @@ Fixpoint env_lookup_delete {A} (i : ident) (Γ : env A) : option (A * env A) :=
      else ''(y,Γ') ← env_lookup_delete i Γ; Some (y, Esnoc Γ' j x)
   end.
 
-Definition env_is_singleton {A} (Γ : env A) : bool :=
-  match Γ with
-  | Esnoc (Esnoc Enil _ _) _ _ => true
-  | _ => false
-  end.
-
 Inductive env_Forall2 {A B} (P : A → B → Prop) : env A → env B → Prop :=
   | env_Forall2_nil : env_Forall2 P Enil Enil
   | env_Forall2_snoc Γ1 Γ2 i x y :
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 9e06f66fa578b78d4890db01ba6c826f802ab3ea..cf98dc70b41ebba2bce4b0313a676fe167dceec0 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -229,7 +229,8 @@ Tactic Notation "iEmpIntro" :=
 Tactic Notation "iPureIntro" :=
   iStartProof;
   eapply tac_pure_intro;
-    [apply _ ||
+    [env_reflexivity
+    |apply _ ||
      let P := match goal with |- FromPure _ ?P _ => P end in
      fail "iPureIntro:" P "not pure"
     |].