diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 3c56dc01954208a1adeb71701f3eb7d17501ef45..9f94d98be364820abfb4452e78943e2d228d717b 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -817,6 +817,10 @@ Proof.
   apply wand_intro_l. by rewrite assoc !wand_elim_r.
 Qed.
 
+Lemma tac_unlock_emp Δ Q : envs_entails Δ Q → envs_entails Δ (emp ∗ locked Q).
+Proof. rewrite envs_entails_eq=> ->. by rewrite -lock left_id. Qed.
+Lemma tac_unlock_True Δ Q : envs_entails Δ Q → envs_entails Δ (True ∗ locked Q).
+Proof. rewrite envs_entails_eq=> ->. by rewrite -lock -True_sep_2. Qed.
 Lemma tac_unlock Δ Q : envs_entails Δ Q → envs_entails Δ (locked Q).
 Proof. by unlock. Qed.
 
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 4a1a64e0c9e2629e80c2427af65d7ca2a3a50872..3755bba63b74ddd79cf2bb7ea8fd3a2a00112678 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -553,8 +553,11 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
           | GSpatial => apply add_modal_id
           | GModal => apply _ || fail "iSpecialize: goal not a modality"
           end
-         |iFrame "∗ #"; apply tac_unlock ||
-          fail "iSpecialize: premise cannot be solved by framing"
+         |first
+            [apply tac_unlock_emp
+            |apply tac_unlock_True
+            |iFrame "∗ #"; apply tac_unlock
+            |fail "iSpecialize: premise cannot be solved by framing"]
          |reflexivity]; iIntro H1; go H1 pats
     end in let pats := spec_pat.parse pat in go H pats.