diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 3ec347a77a46337d23ed684b025f39da205fe60e..aa52877d206335a39ff154e8517057700f2396e7 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -49,10 +49,8 @@ Section proof.
     (∃ lo ln : loc,
        ⌜lk = (#lo, #ln)%V⌝ ∗ inv N (lock_inv γ lo ln R))%I.
 
-  Definition issued (γ : gname) (lk : val) (x : nat) (R : iProp Σ) : iProp Σ :=
-    (∃ lo ln: loc,
-       ⌜lk = (#lo, #ln)%V⌝ ∗ inv N (lock_inv γ lo ln R) ∗
-       own γ (◯ (∅, GSet {[ x ]})))%I.
+  Definition issued (γ : gname) (x : nat) : iProp Σ :=
+    own γ (◯ (∅, GSet {[ x ]}))%I.
 
   Definition locked (γ : gname) : iProp Σ := (∃ o, own γ (◯ (Excl' o, ∅)))%I.
 
@@ -86,9 +84,9 @@ Section proof.
   Qed.
 
   Lemma wait_loop_spec γ lk x R :
-    {{{ issued γ lk x R }}} wait_loop #x lk {{{ RET #(); locked γ ∗ R }}}.
+    {{{ is_lock γ lk R ∗ issued γ x }}} wait_loop #x lk {{{ RET #(); locked γ ∗ R }}}.
   Proof.
-    iIntros (Φ) "Hl HΦ". iDestruct "Hl" as (lo ln) "(% & #? & Ht)".
+    iIntros (Φ) "[Hl Ht] HΦ". iDestruct "Hl" as (lo ln) "(% & #?)".
     iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E.
     iInv N as (o n) "(Hlo & Hln & Ha)" "Hclose".
     wp_load. destruct (decide (x = o)) as [->|Hneq].
@@ -129,7 +127,7 @@ Section proof.
         rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
       iModIntro. wp_if.
       iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]").
-      + rewrite /issued; eauto 10.
+      + iFrame. rewrite /is_lock; eauto 10.
       + by iNext. 
     - wp_cas_fail.
       iMod ("Hclose" with "[Hlo' Hln' Hauth Haown]") as "_".
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 732bbb149ad613256d9942083dd0a03cdf1da7e6..71e728e6f9019a5db90fb669f57608c7d84a1ec3 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -492,12 +492,15 @@ Qed.
 
 (** * Implication and wand *)
 Lemma tac_impl_intro Δ Δ' i P Q :
-  env_spatial_is_nil Δ = true →
+  (if env_spatial_is_nil Δ then Unit else PersistentP P) →
   envs_app false (Esnoc Enil i P) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ P → Q.
 Proof.
-  intros ?? HQ. rewrite (persistentP Δ) envs_app_sound //; simpl.
-  by rewrite right_id always_wand_impl always_elim HQ.
+  intros ?? <-. destruct (env_spatial_is_nil Δ) eqn:?.
+  - rewrite (persistentP Δ) envs_app_sound //; simpl.
+    by rewrite right_id always_wand_impl always_elim.
+  - apply impl_intro_l. rewrite envs_app_sound //; simpl.
+    by rewrite always_and_sep_l right_id wand_elim_r.
 Qed.
 Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
   IntoPersistentP P P' →
diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index bd4273137e2f8a9dadca887450ec6ef819a81028..8e34280a80b165fcf13444b2a10e9332ce90a4bb 100644
--- a/theories/proofmode/notation.v
+++ b/theories/proofmode/notation.v
@@ -7,7 +7,7 @@ Arguments Envs _ _%proof_scope _%proof_scope.
 Arguments Enil {_}.
 Arguments Esnoc {_} _%proof_scope _%string _%uPred_scope.
 
-Notation "" := Enil (format "", only printing) : proof_scope.
+Notation "" := Enil (only printing) : proof_scope.
 Notation "Γ H : P" := (Esnoc Γ H P)
   (at level 1, P at level 200,
    left associativity, format "Γ H  :  P '//'", only printing) : proof_scope.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 15dc96e1527f4933c68ea2c4fb922056e73c2e4b..890a1e6b02db1fae73d444d7d60b92d17f1ab257 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -299,8 +299,10 @@ Local Tactic Notation "iIntro" constr(H) :=
   first
   [ (* (?Q → _) *)
     eapply tac_impl_intro with _ H; (* (i:=H) *)
-      [reflexivity || fail 1 "iIntro: introducing" H
-                             "into non-empty spatial context"
+      [env_cbv; apply _ ||
+       let P := lazymatch goal with |- PersistentP ?P => P end in
+       fail 1 "iIntro: introducing non-persistent" H ":" P
+              "into non-empty spatial context"
       |env_reflexivity || fail "iIntro:" H "not fresh"
       |]
   | (* (_ -∗ _) *)
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index c162461d7f4e53a2d4f1ebff0dee3ed3a2d44a3d..5208ff9e746132b7973b646ce32854d73988de2d 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -77,6 +77,9 @@ Proof.
   done.
 Qed.
 
+Lemma test_iIntros_persistent P Q `{!PersistentP Q} : (P → Q → P ∗ Q)%I.
+Proof. iIntros "H1 H2". by iFrame. Qed.
+
 Lemma test_fast_iIntros P Q :
   (∀ x y z : nat,
     ⌜x = plus 0 x⌝ → ⌜y = 0⌝ → ⌜z = 0⌝ → P → □ Q → foo (x ≡ x))%I.