diff --git a/theories/examples/lateearlychoice.v b/theories/examples/lateearlychoice.v
index 1486e54c084fa201ee30f198a3f519827094c027..029080aa263aa1227e226f882ffda1daa71c16ef 100644
--- a/theories/examples/lateearlychoice.v
+++ b/theories/examples/lateearlychoice.v
@@ -39,7 +39,6 @@ Section proof.
     rel_rec_r. rel_alloc_r y as "Hy".
     repeat rel_pure_r. rel_fork_r i as "Hi".
     repeat rel_pure_r.
-    iApply refines_spec_ctx. iDestruct 1 as (ρ) "#Hρ".
     destruct b.
     - tp_store i. rel_load_r. iApply "He".
     - rel_load_r. iApply "He".
diff --git a/theories/examples/or.v b/theories/examples/or.v
index 9fc2d8f2824d999ac8f400eba869c27ae7e62c9a..a0562e26d7393deb9e5c862bd02e483ac4ae3417 100644
--- a/theories/examples/or.v
+++ b/theories/examples/or.v
@@ -77,9 +77,7 @@ Section rules.
     repeat rel_pure_r.
     iDestruct "H" as "[H | H]".
     - rel_load_r. repeat rel_pure_r. eauto with iFrame.
-    - iApply refines_spec_ctx. (* TODO: get rid of this *)
-      iDestruct 1 as (ρ) "#Hρ".
-      tp_store j.
+    - tp_store j.
       rel_load_r. repeat rel_pure_r. eauto with iFrame.
   Qed.
 
diff --git a/theories/examples/par.v b/theories/examples/par.v
index 19afacd9a3177972b630edced648debfbdd9916a..14aef3b715be3ef6222ff2cde434232a6d98642e 100644
--- a/theories/examples/par.v
+++ b/theories/examples/par.v
@@ -32,7 +32,6 @@ Section rules.
     repeat rel_pure_r. rel_fork_r i as "Hi".
     { simpl. eauto. }
     repeat rel_pure_r.
-    iApply refines_spec_ctx. iDestruct 1 as (ρ) "#Hρ".
     tp_rec i. simpl.
     tp_bind i e1.
     iMod ("H" with "Hi") as (v1) "[Hi H]".
@@ -76,7 +75,6 @@ Section rules.
     repeat rel_pure_r. rel_alloc_r c2 as "Hc2".
     repeat rel_pure_r. rel_fork_r i as "Hi".
     repeat rel_pure_r.
-    iApply refines_spec_ctx. iDestruct 1 as (ρ) "#Hρ".
     tp_rec i. simpl.
     tp_pure i (InjR _). tp_store i.
     rel_bind_l e. rel_bind_r e.
@@ -100,7 +98,6 @@ Section rules.
     repeat rel_pure_r. rel_fork_r i as "Hi".
     { simpl. eauto. }
     repeat rel_pure_r.
-    iApply refines_spec_ctx. iDestruct 1 as (ρ) "#Hρ".
     tp_rec i. simpl.
     rel_rec_l. repeat rel_pure_l.
     rewrite {3}refines_eq /refines_def. iIntros (LL) "_". clear LL.
@@ -152,7 +149,6 @@ Section rules.
     repeat rel_pure_r. rel_fork_r i as "Hi".
     { simpl. eauto. }
     repeat rel_pure_r.
-    iApply refines_spec_ctx. iDestruct 1 as (ρ) "#Hρ".
     tp_rec i. simpl.
     rewrite {3}refines_eq /refines_def. iIntros (LL) "_". clear LL.
     iIntros (j K) "Hj". iModIntro.
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 6a4fa17d0a7a98a83aa3214ad2c42f7449560ba1..89a183026cfa8f55b91dd422bec8ea36fde24410 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -245,6 +245,20 @@ Section related_facts.
     rewrite /IsExcept0. iIntros "HL".
     iApply fupd_logrel. by iMod "HL".
   Qed.
+
+  Lemma refines_spec_ctx E e e' A :
+    ((∃ ρ, spec_ctx ρ) -∗ REL e << e' @ E : A) -∗
+    (REL e << e' @ E : A).
+  Proof.
+    rewrite refines_eq /refines_def.
+    iIntros "Hctx". iIntros (ρ') "#Hspec".
+    rewrite -(bi.intuitionistic_intuitionistically (spec_ctx _)).
+    rewrite (bi.intuitionistically_sep_dup (spec_ctx _)).
+    iDestruct "Hspec" as "[#Hspec #Hspec']".
+    iRevert "Hspec'".
+    rewrite (bi.intuitionistic_intuitionistically (spec_ctx _)).
+    iApply ("Hctx" with "[]"). eauto with iFrame.
+  Qed.
 End related_facts.
 
 Section monadic.
diff --git a/theories/logic/proofmode/spec_tactics.v b/theories/logic/proofmode/spec_tactics.v
index 63fe1861086a67c7cc1583d0728d0e933eeda4b5..dc0887d0931d65b32009e5547479f7d0111de5b2 100644
--- a/theories/logic/proofmode/spec_tactics.v
+++ b/theories/logic/proofmode/spec_tactics.v
@@ -4,7 +4,7 @@ From iris.proofmode Require Import
      coq_tactics ltac_tactics
      sel_patterns environments
      reduction.
-From reloc.logic Require Export spec_rules.
+From reloc.logic Require Export model spec_rules.
 Set Default Proof Using "Type".
 
 (** * TP tactics *)
@@ -99,9 +99,21 @@ Proof.
   by rewrite bi.wand_elim_r.
 Qed.
 
+Ltac with_spec_ctx tac :=
+  lazymatch goal with
+  | |- envs_entails _ (refines ?E ?e1 ?e2 ?A) =>
+    let ρ := fresh in
+    let H := iFresh in
+    iApply (refines_spec_ctx E e1 e2 A);
+    iDestruct 1 as (ρ) H;
+    (tac (); iClear H; clear ρ)
+  | _ => tac ()
+  end.
+
 (* TODO: The problem here is that it will fail if the redex is not specified, and is not on the top level *)
 Tactic Notation "tp_pure" constr(j) open_constr(ef) :=
   iStartProof;
+  with_spec_ctx ltac:(fun _ =>
   eapply (tac_tp_pure j _ ef);
     [iSolveTC || fail "tp_pure: cannot eliminate modality in the goal"
     |solve_ndisj || fail "tp_pure: cannot prove 'nclose specN ⊆ ?'"
@@ -112,7 +124,7 @@ Tactic Notation "tp_pure" constr(j) open_constr(ef) :=
     |try (exact I || reflexivity) (* ψ *)
     |try (exact I || reflexivity) (* Ï• *)
     |pm_reflexivity || fail "tp_pure: this should not happen"
-    |(* new goal *)].
+    |(* new goal *)]).
 
 Tactic Notation "tp_rec" constr(j) := tp_pure j (App _ _).
 Tactic Notation "tp_seq" constr(j) := tp_rec j.
@@ -169,6 +181,7 @@ Qed.
 
 Tactic Notation "tp_store" constr(j) :=
   iStartProof;
+  with_spec_ctx ltac:(fun _ =>
   eapply (tac_tp_store j);
     [iSolveTC || fail "tp_store: cannot eliminate modality in the goal"
     |solve_ndisj || fail "tp_store: cannot prove 'nclose specN ⊆ ?'"
@@ -178,7 +191,7 @@ Tactic Notation "tp_store" constr(j) :=
     |iAssumptionCore || fail "tp_store: cannot find '? ↦ₛ ?'"
     |iSolveTC || fail "tp_store: cannot convert the argument to a value"
     |pm_reflexivity || fail "tp_store: this should not happen"
-    |(* new goal *)].
+    |(* new goal *)]).
 
 (*
 DF:
@@ -226,6 +239,7 @@ Qed.
 
 Tactic Notation "tp_load" constr(j) :=
   iStartProof;
+  with_spec_ctx ltac:(fun _ =>
   eapply (tac_tp_load j);
     [solve_ndisj || fail "tp_load: cannot prove 'nclose specN ⊆ ?'"
     |iAssumptionCore || fail "tp_load: cannot find spec_ctx" (* spec_ctx *)
@@ -233,7 +247,7 @@ Tactic Notation "tp_load" constr(j) :=
     |tp_bind_helper
     |iAssumptionCore || fail "tp_load: cannot find '? ↦ₛ ?'"
     |pm_reflexivity || fail "tp_load: this should not happen"
-    |(* new goal *)].
+    |(* new goal *)]).
 
 Lemma tac_tp_cas_fail `{relocG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e (l : loc) e1 e2 v' v1 v2 Q q :
   nclose specN ⊆ E1 →
@@ -277,6 +291,7 @@ Qed.
 
 Tactic Notation "tp_cas_fail" constr(j) :=
   iStartProof;
+  with_spec_ctx ltac:(fun _ =>
   eapply (tac_tp_cas_fail j);
     [solve_ndisj || fail "tp_cas_fail: cannot prove 'nclose specN ⊆ ?'"
     |iAssumptionCore || fail "tp_cas_fail: cannot find spec_ctx" (* spec_ctx *)
@@ -288,7 +303,7 @@ Tactic Notation "tp_cas_fail" constr(j) :=
     |try congruence (* v' ≠ v1 *)
     |try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
     |pm_reflexivity || fail "tp_cas_fail: this should not happen"
-    |(* new goal *)].
+    |(* new goal *)]).
 
 Lemma tac_tp_cas_suc `{relocG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e (l : loc) e1 e2 v' v1 v2 Q :
   nclose specN ⊆ E1 →
@@ -332,6 +347,7 @@ Qed.
 
 Tactic Notation "tp_cas_suc" constr(j) :=
   iStartProof;
+  with_spec_ctx ltac:(fun _ =>
   eapply (tac_tp_cas_suc j);
     [solve_ndisj || fail "tp_cas_suc: cannot prove 'nclose specN ⊆ ?'"
     |iAssumptionCore || fail "tp_cas_suc: cannot find spec_ctx" (* spec_ctx *)
@@ -343,7 +359,7 @@ Tactic Notation "tp_cas_suc" constr(j) :=
     |try congruence     (* v' = v1 *)
     |try fast_done      (* val_is_unboxed v1 *)
     |pm_reflexivity || fail "tp_cas_suc: this should not happen"
-    |(* new goal *)].
+    |(* new goal *)]).
 
 Lemma tac_tp_faa `{relocG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e (l : loc)  e2 (z1 z2 : Z) Q :
   nclose specN ⊆ E1 →
@@ -384,6 +400,7 @@ Qed.
 
 Tactic Notation "tp_faa" constr(j) :=
   iStartProof;
+  with_spec_ctx ltac:(fun _ =>
   eapply (tac_tp_faa j);
     [solve_ndisj || fail "tp_faa: cannot prove 'nclose specN ⊆ ?'"
     |iAssumptionCore || fail "tp_faa: cannot find spec_ctx" (* spec_ctx *)
@@ -392,7 +409,7 @@ Tactic Notation "tp_faa" constr(j) :=
     |iSolveTC (* IntoVal *)
     |iAssumptionCore || fail "tp_faa: cannot find '? ↦ ?'"
     |pm_reflexivity || fail "tp_faa: this should not happen"
-    |(* new goal *)].
+    |(* new goal *)]).
 
 Lemma tac_tp_fork `{relocG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K' e e' Q :
   nclose specN ⊆ E1 →
@@ -434,16 +451,18 @@ Qed.
 
 Tactic Notation "tp_fork" constr(j) :=
   iStartProof;
+  with_spec_ctx ltac:(fun _ =>
   eapply (tac_tp_fork j);
     [solve_ndisj || fail "tp_fork: cannot prove 'nclose specN ⊆ ?'"
     |iAssumptionCore || fail "tp_fork: cannot find spec_ctx" (* spec_ctx *)
     |iAssumptionCore || fail "tp_fork: cannot find '" j " ⤇ ?'"
     |tp_bind_helper
     |pm_reflexivity || fail "tp_fork: this should not happen"
-    |(* new goal *)].
+    |(* new goal *)]).
 
 Tactic Notation "tp_fork" constr(j) "as" ident(j') constr(H) :=
   iStartProof;
+  with_spec_ctx ltac:(fun _ =>
   eapply (tac_tp_fork j);
     [solve_ndisj || fail "tp_fork: cannot prove 'nclose specN ⊆ ?'"
     |iAssumptionCore || fail "tp_fork: cannot find spec_ctx" (* spec_ctx *)
@@ -452,7 +471,7 @@ Tactic Notation "tp_fork" constr(j) "as" ident(j') constr(H) :=
     |pm_reflexivity || fail "tp_fork: this should not happen"
     |(iIntros (j') || fail 1 "tp_fork: " j' " not fresh ");
      (iIntros H || fail 1 "tp_fork: " H " not fresh")
-    (* new goal *)].
+    (* new goal *)]).
 
 Tactic Notation "tp_fork" constr(j) "as" ident(j') :=
   let H := iFresh in tp_fork j as j' H.
@@ -503,6 +522,7 @@ Tactic Notation "tp_alloc" constr(j) "as" ident(j') constr(H) :=
         [ pm_reflexivity
         | iIntros H || fail 1 "tp_alloc:" H "not correct intro pattern" ] in
   iStartProof;
+  with_spec_ctx ltac:(fun _ =>
   eapply (tac_tp_alloc j);
     [solve_ndisj || fail "tp_alloc: cannot prove 'nclose specN ⊆ ?'"
     |iAssumptionCore || fail "tp_alloc: cannot find spec_ctx" (* spec_ctx *)
@@ -510,7 +530,7 @@ Tactic Notation "tp_alloc" constr(j) "as" ident(j') constr(H) :=
     |tp_bind_helper
     |iSolveTC || fail "tp_alloc: expressions is not a value"
     |finish ()
-    (* new goal *)].
+    (* new goal *)]).
 
 Tactic Notation "tp_alloc" constr(j) "as" ident(j') :=
   let H := iFresh in tp_alloc j as j' H.
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index 1aa8567bf6cbde11cbfdd1567103179de28e22b5..e77ff8c641fbfdc875aefb08102ab68dd0cb1ab5 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -275,24 +275,6 @@ Section rules.
   Qed.
 
   (** ** Primitive structural rules *)
-  Lemma refines_spec_ctx E e e' A :
-    ((∃ ρ, spec_ctx ρ) -∗ REL e << e' @ E : A) -∗
-    (REL e << e' @ E : A).
-  Proof.
-    rewrite refines_eq /refines_def.
-    iIntros "Hctx". iIntros (ρ') "#Hspec".
-    rewrite -(bi.intuitionistic_intuitionistically (spec_ctx _)).
-    rewrite (bi.intuitionistically_sep_dup (spec_ctx _)).
-    iDestruct "Hspec" as "[#Hspec #Hspec']".
-    iRevert "Hspec'".
-    rewrite (bi.intuitionistic_intuitionistically (spec_ctx _)).
-    iAssert (∃ ρ, spec_ctx ρ)%I as "Hρ".
-    { eauto. }
-    iClear "Hspec".
-    iRevert (ρ').
-    by iApply "Hctx".
-  Qed.
-
   Lemma refines_fork e e' :
     (REL e << e' : ()%lrel) -∗
     REL Fork e << Fork e' : ().
diff --git a/theories/tests/proofmode_tests.v b/theories/tests/proofmode_tests.v
index 04bfb1015bd3463c134e480eba521c47a34eab70..d8a8f0a96fca96489cd8da0d382b9c77e9f8c7e7 100644
--- a/theories/tests/proofmode_tests.v
+++ b/theories/tests/proofmode_tests.v
@@ -86,7 +86,6 @@ Proof.
   rel_store_r. do 2 rel_pure_r.
   rel_fork_r i as "Hi".
   repeat rel_pure_r.
-  iApply refines_spec_ctx. iDestruct 1 as (?) "#?".
   tp_store i.
   rel_load_r.
   rel_values.