diff --git a/theories/examples/par.v b/theories/examples/par.v
index f102f15893285f06b9744e8e05b42f7a29204e83..4ddd131876d0326fb512791aa8646b6ed9544427 100644
--- a/theories/examples/par.v
+++ b/theories/examples/par.v
@@ -101,8 +101,8 @@ Section rules.
     repeat rel_pure_r.
     tp_rec i. simpl.
     rel_rec_l. repeat rel_pure_l.
-    rewrite {3}refines_eq /refines_def. iIntros (ρ) "#Hρ".
-    iIntros (j K) "Hj". iModIntro.
+    rewrite {3}refines_eq /refines_def.
+    iIntros (j K) "#Hs Hj". iModIntro.
     tp_bind j e2.
     pose (C:=(AppRCtx (λ: "v2", let: "v1" := spawn.join #c2 in ("v1", "v2")) :: K)).
     fold C.
@@ -110,13 +110,13 @@ Section rules.
     wp_bind (spawn _).
     iApply (spawn_spec N with "[He2 Hj]").
     - wp_lam. rewrite refines_eq /refines_def.
-      iMod ("He2" with "Hρ Hj") as "He2".
+      iMod ("He2" with "Hs Hj") as "He2".
       iAssumption.
     - iNext. iIntros (l) "l_hndl".
       wp_pures. wp_bind e1.
       rewrite refines_eq /refines_def.
       tp_bind i e1.
-      iMod ("He1" with "Hρ Hi") as "He1".
+      iMod ("He1" with "Hs Hi") as "He1".
       iApply (wp_wand with "He1").
       iIntros (v1). iDestruct 1 as (v2) "[Hi Hv]".
       wp_pures. wp_bind (spawn.join _).
@@ -151,18 +151,18 @@ Section rules.
     { simpl. eauto. }
     repeat rel_pure_r.
     tp_rec i. simpl.
-    rewrite {3}refines_eq /refines_def. iIntros (ρ) "#Hρ".
-    iIntros (j K) "Hj". iModIntro.
+    rewrite {3}refines_eq /refines_def.
+    iIntros (j K) "#Hs Hj". iModIntro.
     tp_bind j e2. tp_bind i e1.
     (* execute e1 *)
     wp_bind e1. tp_bind i e1.
     rewrite {1}refines_eq /refines_def.
-    iMod ("He1" with "Hρ Hi") as "He1".
+    iMod ("He1" with "Hs Hi") as "He1".
     iApply (wp_wand with "He1"). iIntros (v1).
     iDestruct 1 as (v2) "[Hi Hv]". wp_pures.
     (* execute e2 *)
     rewrite refines_eq /refines_def.
-    iMod ("He2" with "Hρ Hj") as "He2".
+    iMod ("He2" with "Hs Hj") as "He2".
     iApply wp_fupd.
     iApply (wp_wand with "He2"). iIntros (w1).
     iDestruct 1 as (w2) "[Hj Hw]".
diff --git a/theories/experimental/helping/helping_stack.v b/theories/experimental/helping/helping_stack.v
index 35fcf2f4ccee2c21a0145448ea4d5308be02390a..094fcfbc97048708b4b5b3e2bdbdf246ac136ded 100644
--- a/theories/experimental/helping/helping_stack.v
+++ b/theories/experimental/helping/helping_stack.v
@@ -424,8 +424,7 @@ Section refinement.
         unlock acquire. tp_pure j (App _ lk). iSimpl in "Hj".
         unlock is_locked_r. iDestruct "Hl" as (lk' ->) "Hl".
         (* TODO: make all the tp_ tactics work without the need for an explicit Fupd *)
-        iApply refines_spec_ctx.
-        iDestruct 1 as (ρ) "#Hρ".
+        iApply refines_spec_ctx. iIntros "#Hρ".
         iApply fupd_refines.
         (* because we manually applied `fupd_refines`, the tactical `with_spec_ctx` doesn't work anymore *)
         tp_cmpxchg_suc j. iSimpl in "Hj".
@@ -447,7 +446,7 @@ Section refinement.
         tp_rec j. iSimpl in "Hj".
         tp_pure j (Snd _). unlock release.
         tp_rec j. tp_store j.
-        iClear "Hρ". clear ρ. iModIntro.
+        iClear "Hρ". iModIntro.
 
         rel_apply_r (refines_CG_pop_suc_r with "Hst2 [Hl]").
         { iExists _. by iFrame "Hl". }
@@ -497,8 +496,7 @@ Section refinement.
     iDestruct (offerInv_excl with "HN Ho") as %Hbaz.
     iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
     rewrite {2}refines_eq /refines_def.
-    iIntros (ρ) "#Hs".
-    iIntros (j K) "Hj".
+    iIntros (j K) "#Hs Hj".
     iMod (offerReg_alloc o h2 γ j K with "HNown") as "[HNown Hfrag]"; eauto.
     iMod ("Hcl" with "[-Hfrag Hγ]") as "_".
     { iNext. iExists _,_,_; iFrame.
diff --git a/theories/logic/adequacy.v b/theories/logic/adequacy.v
index 5e771d399f7acb01b15133aaf2850e644ccfe556..2c0098db9c297d1952fb96acda5a5f011f52171e 100644
--- a/theories/logic/adequacy.v
+++ b/theories/logic/adequacy.v
@@ -44,8 +44,8 @@ Proof.
   - iPoseProof (Hlog _) as "Hrel".
     rewrite refines_eq /refines_def /spec_ctx.
     iApply fupd_wp.
-    iSpecialize ("Hrel" with "Hcfg").
-    iApply ("Hrel" $! 0%nat []).
+    iSpecialize ("Hrel" $! 0%nat [] with "[Hcfg]"); first by eauto.
+    iApply "Hrel".
     rewrite tpool_mapsto_eq /tpool_mapsto_def. iFrame.
     by rewrite /to_tpool /= insert_empty map_fmap_singleton //.
   - iIntros (v).
diff --git a/theories/logic/compatibility.v b/theories/logic/compatibility.v
index 5e14b322aaab575f512f45fb1b72a6c6224a8c32..73c57a5c86e3a4849cf6a3638bd08bfda264e25e 100644
--- a/theories/logic/compatibility.v
+++ b/theories/logic/compatibility.v
@@ -60,10 +60,9 @@ Section compatibility.
   Proof.
     iIntros (?) "IH".
     rewrite refines_eq /refines_def.
-    iIntros (ρ) "#Hρ"; iIntros (j K) "Hj /=".
+    iIntros (j K) "Hs Hj /=".
     tp_fork j as i "Hi".
-    iSpecialize ("IH" with "Hρ").
-    iMod ("IH" $! i [] with "Hi") as "IH".
+    iMod ("IH" $! i [] with "Hs Hi") as "IH".
     iApply (wp_fork with "[-Hj]").
     - iNext. iApply (wp_wand with "IH"). eauto.
     - iExists #(); eauto.
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 057ce90f36ee59cf9ea84e63bc85f16d2eda3c96..7d4ea0de2a269b755bce42dd3c20f95ac65bf652 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -62,9 +62,8 @@ Section semtypes.
 
   Definition refines_def (E : coPset)
            (e e' : expr) (A : lrel Σ) : iProp Σ :=
-    (* TODO: refactor the quantifiers *)
-    (∀ ρ, spec_ctx ρ -∗ (∀ j K, j ⤇ fill K e'
-        ={E,⊤}=∗ WP e {{ v, ∃ v', j ⤇ fill K (of_val v') ∗ A v v' }}))%I.
+    (∀ j K, spec_ctx -∗ j ⤇ fill K e'
+        ={E,⊤}=∗ WP e {{ v, ∃ v', j ⤇ fill K (of_val v') ∗ A v v' }})%I.
 
   Definition refines_aux : seal refines_def. Proof. by eexists. Qed.
   Definition refines := unseal refines_aux.
@@ -216,7 +215,7 @@ Section related_facts.
      -∗ (REL e << e' @ E1 : A))%I.
   Proof.
     rewrite refines_eq /refines_def.
-    iIntros "H". iIntros (ρ) "#Hs"; iIntros (j K) "Hj /=".
+    iIntros "H". iIntros (j K) "#Hs Hj /=".
     iMod "H" as "H". iApply ("H" with "Hs Hj").
   Qed.
 
@@ -248,17 +247,12 @@ Section related_facts.
   Qed.
 
   Lemma refines_spec_ctx E e e' A :
-    ((∃ ρ, spec_ctx ρ) -∗ REL 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.
+    iIntros "Hctx". iIntros (j K) "#Hspec".
+    by iApply "Hctx".
   Qed.
 End related_facts.
 
@@ -273,8 +267,8 @@ Section monadic.
   Proof.
     iIntros "Hm Hf".
     rewrite refines_eq /refines_def.
-    iIntros (ρ) "#Hs". iSpecialize ("Hm" with "Hs").
-    iIntros (j K₁) "Hj /=".
+    iIntros (j K₁) "#Hs Hj /=".
+    iSpecialize ("Hm" with "Hs").
     rewrite -fill_app. iMod ("Hm" with "Hj") as "Hm".
     iModIntro. iApply wp_bind.
     iApply (wp_wand with "Hm").
@@ -290,8 +284,7 @@ Section monadic.
   Proof.
     iIntros (<-<-) "HA".
     rewrite refines_eq /refines_def.
-    iIntros (ρ) "#Hs". simpl.
-    iIntros (j K) "Hj /=".
+    iIntros (j K) "#Hs Hj /=".
     iMod "HA" as "HA". iModIntro.
     iApply wp_value. iExists _. by iFrame.
   Qed.
diff --git a/theories/logic/proofmode/spec_tactics.v b/theories/logic/proofmode/spec_tactics.v
index 45fbfffbd8b3335775da362894949d731c33ab37..d633e1c7f9d846465b46cbe1ed480fc67b635f4e 100644
--- a/theories/logic/proofmode/spec_tactics.v
+++ b/theories/logic/proofmode/spec_tactics.v
@@ -64,10 +64,10 @@ Tactic Notation "tp_bind" constr(j) open_constr(efoc) :=
     |reflexivity
     |(* new goal *)].
 
-Lemma tac_tp_pure `{relocG Σ} j K' e1 e2 Δ1 Δ2 E1 ρ i1 i2 p e ϕ ψ Q n :
+Lemma tac_tp_pure `{relocG Σ} j K' e1 e2 Δ1 Δ2 E1 i1 i2 p e ϕ ψ Q n :
   (∀ P, ElimModal ψ false false (|={E1}=> P) P Q Q) →
   nclose specN ⊆ E1 →
-  envs_lookup i1 Δ1 = Some (p, spec_ctx ρ) →
+  envs_lookup i1 Δ1 = Some (p, spec_ctx) →
   envs_lookup i2 Δ1 = Some (false, j ⤇ e)%I →
   e = fill K' e1 →
   PureExec ϕ n e1 e2 →
@@ -83,15 +83,15 @@ Proof.
   rewrite -(idemp bi_and (of_envs Δ1)).
   rewrite {1}(envs_lookup_sound' Δ1 false). 2: apply HΔ1.
   rewrite bi.sep_elim_l.
-  enough (<pers> spec_ctx ρ ∧ of_envs Δ1 -∗ Q) as <-.
+  enough (<pers> spec_ctx ∧ of_envs Δ1 -∗ Q) as <-.
   { rewrite -bi.intuitionistically_into_persistently_1.
     destruct p; simpl;
-    by rewrite ?(bi.intuitionistic_intuitionistically (spec_ctx ρ)). }
+    by rewrite ?(bi.intuitionistic_intuitionistically spec_ctx). }
   rewrite bi.persistently_and_intuitionistically_sep_l.
   rewrite bi.intuitionistic_intuitionistically.
   rewrite (envs_simple_replace_sound Δ1 Δ2 i2) //; simpl.
   rewrite right_id Hfill.
-  rewrite (assoc _ (spec_ctx ρ) (j ⤇ _)%I).
+  rewrite (assoc _ spec_ctx (j ⤇ _)%I).
   rewrite step_pure //.
   rewrite -[Q]elim_modal // /=.
   apply bi.sep_mono_r.
@@ -102,11 +102,10 @@ 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 ρ)
+    iIntros H;
+    (tac (); iClear H)
   | _ => tac ()
   end.
 
@@ -144,11 +143,11 @@ Tactic Notation "tp_if" constr(j) := tp_pure j (If _ _ _).
 Tactic Notation "tp_pair" constr(j) := tp_pure j (Pair _ _).
 Tactic Notation "tp_closure" constr(j) := tp_pure j (Rec _ _ _).
 
-Lemma tac_tp_store `{relocG Σ} j Δ1 Δ2 Δ3 E1 ρ i1 i2 i3 p K' e (l : loc) e' v' v Q :
+Lemma tac_tp_store `{relocG Σ} j Δ1 Δ2 Δ3 E1 i1 i2 i3 p K' e (l : loc) e' v' v Q :
   (∀ P, ElimModal True false false (|={E1}=> P) P Q Q) →
   (* TODO: ^ boolean values here *)
   nclose specN ⊆ E1 →
-  envs_lookup i1 Δ1 = Some (p, spec_ctx ρ) →
+  envs_lookup i1 Δ1 = Some (p, spec_ctx) →
   envs_lookup_delete false i2 Δ1 = Some (false, j ⤇ e, Δ2)%I →
   e = fill K' (Store (# l) e') →
   envs_lookup i3 Δ2 = Some (false, l ↦ₛ v')%I →
@@ -162,15 +161,15 @@ Proof.
   rewrite -(idemp bi_and (of_envs Δ1)).
   rewrite {1}(envs_lookup_sound' _ false). 2: eassumption.
   rewrite bi.sep_elim_l.
-  enough (spec_ctx ρ ∗ of_envs Δ1 -∗ Q) as Hq.
+  enough (spec_ctx ∗ of_envs Δ1 -∗ Q) as Hq.
   { rewrite -Hq.
-    destruct p; simpl; last rewrite -(bi.intuitionistic_intuitionistically (spec_ctx ρ));
+    destruct p; simpl; last rewrite -(bi.intuitionistic_intuitionistically spec_ctx);
     rewrite {1}bi.intuitionistically_into_persistently_1 bi.persistently_and_intuitionistically_sep_l;
-    by rewrite (bi.intuitionistic_intuitionistically (spec_ctx ρ)). }
+    by rewrite (bi.intuitionistic_intuitionistically spec_ctx). }
   rewrite envs_lookup_delete_sound //; simpl.
   rewrite envs_simple_replace_sound //; simpl.
   rewrite right_id.
-  rewrite !assoc -(assoc _ (spec_ctx _)) Hfill.
+  rewrite !assoc -(assoc _ spec_ctx) Hfill.
   rewrite step_store //.
   rewrite -[Q]elim_modal //.
   apply bi.sep_mono_r.
@@ -201,9 +200,9 @@ how can we prove that [i1 <> i2]? If we can do that then we can utilize
 the lemma [envs_lookup_envs_delete_ne].
 *)
 
-Lemma tac_tp_load `{relocG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e (l : loc) v Q q :
+Lemma tac_tp_load `{relocG Σ} j Δ1 Δ2 Δ3 E1 E2 i1 i2 i3 p K' e (l : loc) v Q q :
   nclose specN ⊆ E1 →
-  envs_lookup i1 Δ1 = Some (p, spec_ctx ρ) →
+  envs_lookup i1 Δ1 = Some (p, spec_ctx) →
   envs_lookup_delete false i2 Δ1 = Some (false, j ⤇ e, Δ2)%I →
   e = fill K' (Load #l) →
   envs_lookup i3 Δ2 = Some (false, l ↦ₛ{q} v)%I →
@@ -216,21 +215,19 @@ Proof.
   rewrite -(idemp bi_and (of_envs Δ1)).
   rewrite {1}(envs_lookup_sound' Δ1 false). 2: eassumption.
   rewrite bi.sep_elim_l.
-  enough (<pers> spec_ctx ρ ∧ of_envs Δ1 ={E1,E2}=∗ Q) as <-.
+  enough (<pers> spec_ctx ∧ of_envs Δ1 ={E1,E2}=∗ Q) as <-.
   { rewrite -bi.intuitionistically_into_persistently_1.
     destruct p; simpl;
-    by rewrite ?(bi.intuitionistic_intuitionistically (spec_ctx ρ)). }
+    by rewrite ?(bi.intuitionistic_intuitionistically spec_ctx). }
   rewrite bi.persistently_and_intuitionistically_sep_l.
   rewrite bi.intuitionistic_intuitionistically.
   rewrite envs_lookup_delete_sound //; simpl.
   rewrite (envs_simple_replace_sound Δ2 Δ3 i3) //; simpl.
   rewrite right_id Hfill.
-  (* (S (spec_ctx ρ) (S (j => fill) (S (l ↦ v) ..))) *)
-  rewrite (assoc _ (spec_ctx ρ) (j ⤇ fill K' (Load _))%I).
-  (* (S (S (spec_ctx ρ) (j => fill)) (S (l ↦ v) ..)) *)
+  rewrite (assoc _ spec_ctx (j ⤇ fill K' (Load _))%I).
   rewrite assoc.
-  rewrite -(assoc _ (spec_ctx ρ) (j ⤇ fill K' (Load _))%I).
-  rewrite (step_load _ ρ j K' l q v) //.
+  rewrite -(assoc _ spec_ctx (j ⤇ fill K' (Load _))%I).
+  rewrite (step_load _ j K' l q v) //.
   rewrite -(fupd_trans E1 E1 E2).
   rewrite fupd_frame_r.
   apply fupd_mono.
@@ -249,9 +246,9 @@ Tactic Notation "tp_load" constr(j) :=
     |pm_reflexivity || fail "tp_load: this should not happen"
     |(* new goal *)]).
 
-Lemma tac_tp_cmpxchg_fail `{relocG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e (l : loc) e1 e2 v' v1 v2 Q q :
+Lemma tac_tp_cmpxchg_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 →
-  envs_lookup i1 Δ1 = Some (p, spec_ctx ρ) →
+  envs_lookup i1 Δ1 = Some (p, spec_ctx) →
   envs_lookup_delete false i2 Δ1 = Some (false, j ⤇ e, Δ2)%I →
   e = fill K' (CmpXchg #l e1 e2) →
   IntoVal e1 v1 →
@@ -268,20 +265,20 @@ Proof.
   rewrite -(idemp bi_and (of_envs Δ1)).
   rewrite {1}(envs_lookup_sound' Δ1 false). 2: eassumption.
   rewrite bi.sep_elim_l.
-  enough (<pers> spec_ctx ρ ∧ of_envs Δ1 ={E1,E2}=∗ Q) as <-.
+  enough (<pers> spec_ctx ∧ of_envs Δ1 ={E1,E2}=∗ Q) as <-.
   { rewrite -bi.intuitionistically_into_persistently_1.
     destruct p; simpl;
-    by rewrite ?(bi.intuitionistic_intuitionistically (spec_ctx ρ)). }
+    by rewrite ?(bi.intuitionistic_intuitionistically spec_ctx). }
   rewrite bi.persistently_and_intuitionistically_sep_l.
   rewrite bi.intuitionistic_intuitionistically.
   rewrite envs_lookup_delete_sound // /=.
   rewrite (envs_simple_replace_sound Δ2 Δ3 i3) // /=.
   rewrite Hfill.
-  (* (S (spec_ctx ρ) (S (j => fill _ _) (S (l ↦ v) ..))) *)
-  rewrite (assoc _ (spec_ctx ρ) (j ⤇ fill K' _)%I).
-  (* (S (S (spec_ctx ρ) (j => fill _ _)) (S (l ↦ v) ..)) *)
+  (* (S spec_ctx (S (j => fill _ _) (S (l ↦ v) ..))) *)
+  rewrite (assoc _ spec_ctx (j ⤇ fill K' _)%I).
+  (* (S (S spec_ctx (j => fill _ _)) (S (l ↦ v) ..)) *)
   rewrite assoc.
-  rewrite -(assoc _ (spec_ctx ρ) (j ⤇ fill K' _)%I).
+  rewrite -(assoc _ spec_ctx (j ⤇ fill K' _)%I).
   rewrite step_cmpxchg_fail //.
   rewrite -(fupd_trans E1 E1 E2).
   rewrite fupd_frame_r.
@@ -305,9 +302,9 @@ Tactic Notation "tp_cmpxchg_fail" constr(j) :=
     |pm_reflexivity || fail "tp_cmpxchg_fail: this should not happen"
     |(* new goal *)]).
 
-Lemma tac_tp_cmpxchg_suc `{relocG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e (l : loc) e1 e2 v' v1 v2 Q :
+Lemma tac_tp_cmpxchg_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 →
-  envs_lookup i1 Δ1 = Some (p, spec_ctx ρ) →
+  envs_lookup i1 Δ1 = Some (p, spec_ctx) →
   envs_lookup_delete false i2 Δ1 = Some (false, j ⤇ e, Δ2)%I →
   e = fill K' (CmpXchg #l e1 e2) →
   IntoVal e1 v1 →
@@ -324,20 +321,20 @@ Proof.
   rewrite -(idemp bi_and (of_envs Δ1)).
   rewrite {1}(envs_lookup_sound' Δ1 false). 2: eassumption.
   rewrite bi.sep_elim_l.
-  enough (<pers> spec_ctx ρ ∧ of_envs Δ1 ={E1,E2}=∗ Q) as <-.
+  enough (<pers> spec_ctx ∧ of_envs Δ1 ={E1,E2}=∗ Q) as <-.
   { rewrite -bi.intuitionistically_into_persistently_1.
     destruct p; simpl;
-    by rewrite ?(bi.intuitionistic_intuitionistically (spec_ctx ρ)). }
+    by rewrite ?(bi.intuitionistic_intuitionistically spec_ctx). }
   rewrite bi.persistently_and_intuitionistically_sep_l.
   rewrite bi.intuitionistic_intuitionistically.
   rewrite envs_lookup_delete_sound // /=.
   rewrite (envs_simple_replace_sound Δ2 Δ3 i3) //.
   simpl. rewrite right_id Hfill.
-  (* (S (spec_ctx ρ) (S (j => fill _ _) (S (l ↦ v) ..))) *)
-  rewrite (assoc _ (spec_ctx ρ) (j ⤇ fill K' _)%I).
-  (* (S (S (spec_ctx ρ) (j => fill _ _)) (S (l ↦ v) ..)) *)
+  (* (S spec_ctx (S (j => fill _ _) (S (l ↦ v) ..))) *)
+  rewrite (assoc _ spec_ctx (j ⤇ fill K' _)%I).
+  (* (S (S spec_ctx (j => fill _ _)) (S (l ↦ v) ..)) *)
   rewrite assoc.
-  rewrite -(assoc _ (spec_ctx ρ) (j ⤇ fill K' _)%I).
+  rewrite -(assoc _ spec_ctx (j ⤇ fill K' _)%I).
   rewrite step_cmpxchg_suc //.
   rewrite -(fupd_trans E1 E1 E2).
   rewrite fupd_frame_r.
@@ -361,9 +358,9 @@ Tactic Notation "tp_cmpxchg_suc" constr(j) :=
     |pm_reflexivity || fail "tp_cmpxchg_suc: this should not happen"
     |(* 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 :
+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 →
-  envs_lookup i1 Δ1 = Some (p, spec_ctx ρ) →
+  envs_lookup i1 Δ1 = Some (p, spec_ctx) →
   envs_lookup_delete false i2 Δ1 = Some (false, j ⤇ e, Δ2)%I →
   e = fill K' (FAA #l e2) →
   IntoVal e2 #z2 →
@@ -377,20 +374,20 @@ Proof.
   rewrite -(idemp bi_and (of_envs Δ1)).
   rewrite {1}(envs_lookup_sound' Δ1 false). 2: eassumption.
   rewrite bi.sep_elim_l.
-  enough (<pers> spec_ctx ρ ∧ of_envs Δ1 ={E1,E2}=∗ Q) as <-.
+  enough (<pers> spec_ctx ∧ of_envs Δ1 ={E1,E2}=∗ Q) as <-.
   { rewrite -bi.intuitionistically_into_persistently_1.
     destruct p; simpl;
-    by rewrite ?(bi.intuitionistic_intuitionistically (spec_ctx ρ)). }
+    by rewrite ?(bi.intuitionistic_intuitionistically spec_ctx). }
   rewrite bi.persistently_and_intuitionistically_sep_l.
   rewrite bi.intuitionistic_intuitionistically.
   rewrite envs_lookup_delete_sound // /=.
   rewrite (envs_simple_replace_sound Δ2 Δ3 i3) //.
   simpl. rewrite right_id Hfill.
-  (* (S (spec_ctx ρ) (S (j => fill _ _) (S (l ↦ v) ..))) *)
-  rewrite (assoc _ (spec_ctx ρ) (j ⤇ fill K' _)%I).
-  (* (S (S (spec_ctx ρ) (j => fill _ _)) (S (l ↦ v) ..)) *)
+  (* (S spec_ctx (S (j => fill _ _) (S (l ↦ v) ..))) *)
+  rewrite (assoc _ spec_ctx (j ⤇ fill K' _)%I).
+  (* (S (S spec_ctx (j => fill _ _)) (S (l ↦ v) ..)) *)
   rewrite assoc.
-  rewrite -(assoc _ (spec_ctx ρ) (j ⤇ fill K' _)%I).
+  rewrite -(assoc _ spec_ctx (j ⤇ fill K' _)%I).
   rewrite step_faa //.
   rewrite -(fupd_trans E1 E1 E2).
   rewrite fupd_frame_r.
@@ -411,9 +408,9 @@ Tactic Notation "tp_faa" constr(j) :=
     |pm_reflexivity || fail "tp_faa: this should not happen"
     |(* new goal *)]).
 
-Lemma tac_tp_fork `{relocG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K' e e' Q :
+Lemma tac_tp_fork `{relocG Σ} j Δ1 Δ2 E1 E2 i1 i2 p K' e e' Q :
   nclose specN ⊆ E1 →
-  envs_lookup i1 Δ1 = Some (p, spec_ctx ρ) →
+  envs_lookup i1 Δ1 = Some (p, spec_ctx) →
   envs_lookup i2 Δ1 = Some (false, j ⤇ e)%I →
   e = fill K' (Fork e') →
   envs_simple_replace i2 false
@@ -425,16 +422,16 @@ Proof.
   rewrite -(idemp bi_and (of_envs Δ1)).
   rewrite {1}(envs_lookup_sound' Δ1 false i1). 2: eassumption.
   rewrite bi.sep_elim_l /=.
-  enough (<pers> spec_ctx ρ ∧ of_envs Δ1 ={E1,E2}=∗ Q) as <-.
+  enough (<pers> spec_ctx ∧ of_envs Δ1 ={E1,E2}=∗ Q) as <-.
   { rewrite -bi.intuitionistically_into_persistently_1.
     destruct p; simpl;
-    by rewrite ?(bi.intuitionistic_intuitionistically (spec_ctx ρ)). }
+    by rewrite ?(bi.intuitionistic_intuitionistically spec_ctx). }
   rewrite bi.persistently_and_intuitionistically_sep_l.
   rewrite bi.intuitionistic_intuitionistically.
   rewrite (envs_simple_replace_sound Δ1 Δ2 i2) //; simpl.
   rewrite right_id Hfill.
-  (* (S (spec_ctx ρ) (S (j => fill) (S (l ↦ v) ..))) *)
-  rewrite (assoc _ (spec_ctx ρ) (j ⤇ _)%I).
+  (* (S spec_ctx (S (j => fill) (S (l ↦ v) ..))) *)
+  rewrite (assoc _ spec_ctx (j ⤇ _)%I).
   rewrite step_fork //.
   rewrite -(fupd_trans E1 E1 E2).
   rewrite fupd_frame_r.
@@ -476,9 +473,9 @@ Tactic Notation "tp_fork" constr(j) "as" ident(j') constr(H) :=
 Tactic Notation "tp_fork" constr(j) "as" ident(j') :=
   let H := iFresh in tp_fork j as j' H.
 
-Lemma tac_tp_alloc `{relocG Σ} j Δ1 E1 E2 ρ i1 i2 p K' e e' v Q :
+Lemma tac_tp_alloc `{relocG Σ} j Δ1 E1 E2 i1 i2 p K' e e' v Q :
   nclose specN ⊆ E1 →
-  envs_lookup i1 Δ1 = Some (p, spec_ctx ρ) →
+  envs_lookup i1 Δ1 = Some (p, spec_ctx) →
   envs_lookup i2 Δ1 = Some (false, j ⤇ e)%I →
   e = fill K' (ref e') →
   IntoVal e' v →
@@ -492,10 +489,10 @@ Proof.
   rewrite -(idemp bi_and (of_envs Δ1)).
   rewrite {1}(envs_lookup_sound' Δ1 false i1). 2: eassumption.
   rewrite bi.sep_elim_l /=.
-  enough (<pers> spec_ctx ρ ∧ of_envs Δ1 ={E1,E2}=∗ Q) as <-.
+  enough (<pers> spec_ctx ∧ of_envs Δ1 ={E1,E2}=∗ Q) as <-.
   { rewrite -bi.intuitionistically_into_persistently_1.
     destruct p; simpl;
-    by rewrite ?(bi.intuitionistic_intuitionistically (spec_ctx ρ)). }
+    by rewrite ?(bi.intuitionistic_intuitionistically spec_ctx). }
   rewrite bi.persistently_and_intuitionistically_sep_l.
   rewrite bi.intuitionistic_intuitionistically.
   rewrite (envs_lookup_sound' Δ1 false i2). 2: eassumption.
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index d5392c37cd671daae3e74a0659b0fe3cb9db7656..64205c6734a6405163f0f6633c727eb32a0dc7a5 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -28,7 +28,7 @@ Section rules.
   Proof.
     intros Hpure HÏ•.
     rewrite refines_eq /refines_def.
-    iIntros "IH" (ρ) "#Hs"; iIntros (j K) "Hj /=".
+    iIntros "IH" ; iIntros (j K) "#Hs Hj /=".
     iModIntro. wp_pures.
     iApply fupd_wp. iApply ("IH" with "Hs Hj").
   Qed.
@@ -42,7 +42,7 @@ Section rules.
   Proof.
     intros Hpure HÏ•.
     rewrite refines_eq /refines_def.
-    iIntros "IH" (ρ) "#Hs"; iIntros (j K) "Hj /=".
+    iIntros "IH" ; iIntros (j K) "#Hs Hj /=".
     iMod ("IH" with "Hs Hj") as "IH".
     iModIntro. by wp_pures.
   Qed.
@@ -54,7 +54,7 @@ Section rules.
   Proof.
     rewrite refines_eq /refines_def.
     iIntros "He".
-    iIntros (ρ) "#Hs". iIntros (j K') "Hj /=".
+    iIntros (j K') "#Hs Hj /=".
     iModIntro. iApply wp_bind.
     iApply (wp_wand with "He").
     iIntros (v) "Hv".
@@ -69,7 +69,7 @@ Section rules.
   Proof.
     rewrite refines_eq /refines_def.
     iIntros "Hlog".
-    iIntros (ρ) "#Hs". iIntros (j K') "Hj /=". iModIntro.
+    iIntros (j K') "#Hs Hj /=". iModIntro.
     iApply wp_bind. iApply wp_atomic; auto.
     iMod "Hlog" as "He". iModIntro.
     iApply (wp_wand with "He").
@@ -87,23 +87,23 @@ Section rules.
     ⊢ REL t << fill K' e @ E : A.
   Proof.
     rewrite refines_eq /refines_def => Hpure HÏ•.
-    iIntros "Hlog". iIntros (ρ) "#Hs". iIntros (j K) "Hj /=".
+    iIntros "Hlog". iIntros (j K) "#Hs Hj /=".
     tp_pure j _; auto.
     iApply ("Hlog" with "Hs Hj").
   Qed.
 
   (* A helper lemma for proving the stateful reductions for the RHS below *)
   Lemma refines_step_r Φ E K' e1 e2 A :
-    (∀ ρ j K, spec_ctx ρ -∗ (j ⤇ fill K e2 ={E}=∗ ∃ v, j ⤇ fill K (of_val v)
+    (∀ j K, spec_ctx -∗ (j ⤇ fill K e2 ={E}=∗ ∃ v, j ⤇ fill K (of_val v)
                   ∗ Φ v)) -∗
     (∀ v, Φ v -∗ REL e1 << fill K' (of_val v) @ E : A) -∗
     REL e1 << fill K' e2 @ E : A.
   Proof.
     rewrite refines_eq /refines_def.
     iIntros "He Hlog".
-    iIntros (ρ) "#Hs". iIntros (j K) "Hj /=".
+    iIntros (j K) "#Hs Hj /=".
     rewrite -fill_app.
-    iMod ("He" $! ρ j with "Hs Hj") as (v) "[Hj Hv]".
+    iMod ("He" $! j with "Hs Hj") as (v) "[Hj Hv]".
     iSpecialize ("Hlog" $! v with "Hv Hs").
     rewrite fill_app.
     by iApply "Hlog".
@@ -118,7 +118,7 @@ Section rules.
     pose (Φ := (fun w => ∃ (p : proph_id), ⌜w = (# p)⌝ : iProp Σ)%I).
     iApply (refines_step_r Φ); simpl; auto.
     { cbv[Φ].
-      iIntros (ρ j K') "#Hs Hj /=".
+      iIntros (j K') "#Hs Hj /=".
       iMod (step_newproph with "[$Hs $Hj]") as (p) "Hj". done.
       iModIntro. iExists _. iFrame. iExists _. iFrame. eauto. }
     iIntros (v') "He'". iDestruct "He'" as (p) "%". subst.
@@ -134,7 +134,7 @@ Section rules.
     pose (Φ := (fun w => ⌜w = #()⌝ : iProp Σ)%I).
     iApply (refines_step_r Φ); simpl; auto.
     { cbv[Φ].
-      iIntros (ρ j K') "#Hs Hj /=".
+      iIntros (j K') "#Hs Hj /=".
       iMod (step_resolveproph with "[$Hs $Hj]") as "Hj". done.
       iModIntro. iExists _. iFrame. eauto. }
     iIntros (v') "He'". iDestruct "He'" as %->.
@@ -152,7 +152,7 @@ Section rules.
     pose (Φ := (fun w => ∃ l : loc, ⌜w = (# l)⌝ ∗ l ↦ₛ v)%I).
     iApply (refines_step_r Φ); simpl; auto.
     { cbv[Φ].
-      iIntros (ρ j K') "#Hs Hj /=".
+      iIntros (j K') "#Hs Hj /=".
       tp_alloc j as l "Hl". iExists (# l).
       iFrame. iExists l. eauto. }
     iIntros (v') "He'". iDestruct "He'" as (l) "[% Hl]". subst.
@@ -169,7 +169,7 @@ Section rules.
     pose (Φ := (fun w => ⌜w = v⌝ ∗ l ↦ₛ{q} v)%I).
     iApply (refines_step_r Φ with "[Hl]"); eauto.
     { cbv[Φ].
-      iIntros (ρ j K') "#Hs Hj /=". iExists v.
+      iIntros (j K') "#Hs Hj /=". iExists v.
       tp_load j.
       iFrame. eauto. }
     iIntros (?) "[% Hl]"; subst.
@@ -187,7 +187,7 @@ Section rules.
     pose (Φ := (fun w => ⌜w = #()⌝ ∗ l ↦ₛ v')%I).
     iApply (refines_step_r Φ with "[Hl]"); eauto.
     { cbv[Φ].
-      iIntros (ρ j K') "#Hs Hj /=". iExists #().
+      iIntros (j K') "#Hs Hj /=". iExists #().
       tp_store j.
       iFrame. eauto. }
     iIntros (w) "[% Hl]"; subst.
@@ -208,7 +208,7 @@ Section rules.
     pose (Φ := (fun (w : val) => ⌜w = (v, #false)%V⌝ ∗ l ↦ₛ v)%I).
     iApply (refines_step_r Φ with "[Hl]"); eauto.
     { cbv[Φ].
-      iIntros (ρ j K') "#Hs Hj /=".
+      iIntros (j K') "#Hs Hj /=".
       tp_cmpxchg_fail j; auto.
       iExists _. simpl.
       iFrame. eauto. }
@@ -230,7 +230,7 @@ Section rules.
     pose (Φ := (fun w => ⌜w = (v, #true)%V⌝ ∗ l ↦ₛ v2)%I).
     iApply (refines_step_r Φ with "[Hl]"); eauto.
     { cbv[Φ].
-      iIntros (ρ j K') "#Hs Hj /=".
+      iIntros (j K') "#Hs Hj /=".
       tp_cmpxchg_suc j; auto.
       iExists _. simpl.
       iFrame. eauto. }
@@ -249,7 +249,7 @@ Section rules.
     pose (Φ := (fun w => ⌜w = #i1⌝ ∗ l ↦ₛ #(i1+i2))%I).
     iApply (refines_step_r Φ with "[Hl]"); eauto.
     { cbv[Φ].
-      iIntros (ρ j K') "#Hs Hj /=".
+      iIntros (j K') "#Hs Hj /=".
       tp_faa j; auto.
       iExists #i1. simpl.
       iFrame. eauto. }
@@ -266,7 +266,7 @@ Section rules.
     iIntros "Hlog".
     pose (Φ := (fun (v : val) => ∃ i, i ⤇ e ∗ ⌜v = #()⌝%V)%I).
     iApply (refines_step_r Φ with "[]"); cbv[Φ].
-    { iIntros (ρ j K') "#Hspec Hj".
+    { iIntros (j K') "#Hspec Hj".
       tp_fork j as i "Hi".
       iModIntro. iExists #(). iFrame. eauto.
     }
@@ -281,10 +281,9 @@ Section rules.
   Proof.
     rewrite refines_eq /refines_def.
     iIntros "H".
-    iIntros (ρ) "#Hs"; iIntros (j K) "Hj /=".
+    iIntros (j K) "#Hs Hj /=".
     tp_fork j as i "Hi". iModIntro.
-    iSpecialize ("H" with "Hs").
-    iSpecialize ("H" $! i [] with "Hi"). simpl.
+    iSpecialize ("H" $! i [] with "Hs Hi").
     iApply (wp_fork with "[H]").
     - iNext. iMod "H". iApply (wp_wand with "H"). eauto.
     - iNext. iExists _. by iFrame.
@@ -299,7 +298,7 @@ Section rules.
     REL v << v' : (A → A')%lrel.
   Proof.
     rewrite /AsRecV. iIntros (-> ->) "#H".
-    iApply refines_spec_ctx. iDestruct 1 as (ρ) "#Hs".
+    iApply refines_spec_ctx. iIntros "Hs".
     iApply refines_ret. iModIntro.
     iModIntro. iIntros (v1 v2) "HA".
     iSpecialize ("H" with "HA").
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index e56bdb60a5833d443b3b0eab654f9a8c5bb1c96b..e5cff14c44acc0839abc7b3744505861f8cb9237 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -45,14 +45,14 @@ Section definitionsS.
   Definition spec_inv ρ : iProp Σ :=
     (∃ tp σ, own cfg_name (● (to_tpool tp, to_gen_heap (heap σ)))
                  ∗ ⌜rtc erased_step ρ (tp,σ)⌝)%I.
-  Definition spec_ctx (ρ : cfg heap_lang) : iProp Σ :=
-    inv specN (spec_inv ρ).
+  Definition spec_ctx : iProp Σ :=
+    (∃ ρ, inv specN (spec_inv ρ))%I.
 
   Global Instance heapS_mapsto_timeless l q v : Timeless (heapS_mapsto l q v).
   Proof. rewrite heapS_mapsto_eq. apply _. Qed.
   Global Instance tpool_mapsto_timeless j e: Timeless (tpool_mapsto j e).
   Proof. rewrite tpool_mapsto_eq. apply _. Qed.
-  Global Instance spec_ctx_persistent ρ : Persistent (spec_ctx ρ).
+  Global Instance spec_ctx_persistent : Persistent spec_ctx.
   Proof. apply _. Qed.
 End definitionsS.
 Typeclasses Opaque heapS_mapsto tpool_mapsto spec_ctx.
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index 3b7be1f8f26551711714f0adbf7376404aa0e65d..3f0079a6a137bf06b08f6bec244ff4d88fe4f9c1 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -51,14 +51,15 @@ Section rules.
 
   (** * Main rules *)
   (** Pure reductions *)
-  Lemma step_pure E ρ j K e e' (P : Prop) n :
+  Lemma step_pure E j K e e' (P : Prop) n :
     P →
     PureExec P n e e' →
     nclose specN ⊆ E →
-    spec_ctx ρ ∗ j ⤇ fill K e ={E}=∗ j ⤇ fill K e'.
+    spec_ctx ∗ j ⤇ fill K e ={E}=∗ j ⤇ fill K e'.
   Proof.
     iIntros (HP Hex ?) "[#Hspec Hj]".
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=.
+    iDestruct "Hspec" as (ρ) "Hspec".
     iInv specN as (tp σ) ">[Hown Hrtc]" "Hclose".
     iDestruct "Hrtc" as %Hrtc.
     iDestruct (own_valid_2 with "Hown Hj")
@@ -97,13 +98,14 @@ Section rules.
   Qed.
 
   (** Prophecy variables (at this point those are just noops) *)
-  Lemma step_newproph E ρ j K :
+  Lemma step_newproph E j K :
     nclose specN ⊆ E →
-    spec_ctx ρ ∗ j ⤇ fill K NewProph ={E}=∗
+    spec_ctx ∗ j ⤇ fill K NewProph ={E}=∗
     ∃ (p : proph_id), j ⤇ fill K #p.
   Proof.
     iIntros (?) "[#Hinv Hj]".
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=.
+    iDestruct "Hinv" as (ρ) "Hinv".
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid.
@@ -117,13 +119,14 @@ Section rules.
     eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
   Qed.
 
-  Lemma step_resolveproph E ρ j K (p : proph_id) w :
+  Lemma step_resolveproph E j K (p : proph_id) w :
     nclose specN ⊆ E →
-    spec_ctx ρ ∗ j ⤇ fill K (ResolveProph #p (of_val w)) ={E}=∗
+    spec_ctx ∗ j ⤇ fill K (ResolveProph #p (of_val w)) ={E}=∗
     j ⤇ fill K #().
   Proof.
     iIntros (?) "[#Hinv Hj]".
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=.
+    iDestruct "Hinv" as (ρ) "Hinv".
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid.
@@ -137,13 +140,14 @@ Section rules.
   Qed.
 
   (** Alloc, load, and store *)
-  Lemma step_alloc E ρ j K e v :
+  Lemma step_alloc E j K e v :
     IntoVal e v →
     nclose specN ⊆ E →
-    spec_ctx ρ ∗ j ⤇ fill K (ref e) ={E}=∗ ∃ l, j ⤇ fill K (#l) ∗ l ↦ₛ v.
+    spec_ctx ∗ j ⤇ fill K (ref e) ={E}=∗ ∃ l, j ⤇ fill K (#l) ∗ l ↦ₛ v.
   Proof.
     iIntros (<-?) "[#Hinv Hj]".
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=.
+    iDestruct "Hinv" as (ρ) "Hinv".
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     destruct (exist_fresh (dom (gset loc) (heap σ))) as [l Hl%not_elem_of_dom].
     iDestruct (own_valid_2 with "Hown Hj")
@@ -164,13 +168,14 @@ Section rules.
     intros. assert (i = 0) as -> by lia. by rewrite loc_add_0.
   Qed.
 
-  Lemma step_load E ρ j K l q v:
+  Lemma step_load E j K l q v:
     nclose specN ⊆ E →
-    spec_ctx ρ ∗ j ⤇ fill K (!#l) ∗ l ↦ₛ{q} v
+    spec_ctx ∗ j ⤇ fill K (!#l) ∗ l ↦ₛ{q} v
     ={E}=∗ j ⤇ fill K (of_val v) ∗ l ↦ₛ{q} v.
   Proof.
     iIntros (?) "(#Hinv & Hj & Hl)".
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
+    iDestruct "Hinv" as (ρ) "Hinv".
     rewrite heapS_mapsto_eq /heapS_mapsto_def /=.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
@@ -185,14 +190,15 @@ Section rules.
     eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
   Qed.
 
-  Lemma step_store E ρ j K l v' e v:
+  Lemma step_store E j K l v' e v:
     IntoVal e v →
     nclose specN ⊆ E →
-    spec_ctx ρ ∗ j ⤇ fill K (#l <- e) ∗ l ↦ₛ v'
+    spec_ctx ∗ j ⤇ fill K (#l <- e) ∗ l ↦ₛ v'
     ={E}=∗ j ⤇ fill K #() ∗ l ↦ₛ v.
   Proof.
     iIntros (<-?) "(#Hinv & Hj & Hl)".
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
+    iDestruct "Hinv" as (ρ) "Hinv".
     rewrite heapS_mapsto_eq /heapS_mapsto_def /=.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
@@ -213,17 +219,18 @@ Section rules.
   Qed.
 
   (** CmpXchg & FAA *)
-  Lemma step_cmpxchg_fail E ρ j K l q v' e1 v1 e2 v2 :
+  Lemma step_cmpxchg_fail E j K l q v' e1 v1 e2 v2 :
     IntoVal e1 v1 →
     IntoVal e2 v2 →
     nclose specN ⊆ E →
     vals_compare_safe v' v1 →
     v' ≠ v1 →
-    spec_ctx ρ ∗ j ⤇ fill K (CmpXchg #l e1 e2) ∗ l ↦ₛ{q} v'
+    spec_ctx ∗ j ⤇ fill K (CmpXchg #l e1 e2) ∗ l ↦ₛ{q} v'
     ={E}=∗ j ⤇ fill K (v', #false)%V ∗ l ↦ₛ{q} v'.
   Proof.
     iIntros (<-<-???) "(#Hinv & Hj & Hl)".
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
+    iDestruct "Hinv" as (ρ) "Hinv".
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid.
@@ -239,17 +246,18 @@ Section rules.
     rewrite bool_decide_false //.
   Qed.
 
-  Lemma step_cmpxchg_suc E ρ j K l e1 v1 v1' e2 v2:
+  Lemma step_cmpxchg_suc E j K l e1 v1 v1' e2 v2:
     IntoVal e1 v1 →
     IntoVal e2 v2 →
     nclose specN ⊆ E →
     vals_compare_safe v1' v1 →
     v1' = v1 →
-    spec_ctx ρ ∗ j ⤇ fill K (CmpXchg #l e1 e2) ∗ l ↦ₛ v1'
+    spec_ctx ∗ j ⤇ fill K (CmpXchg #l e1 e2) ∗ l ↦ₛ v1'
     ={E}=∗ j ⤇ fill K (v1', #true)%V ∗ l ↦ₛ v2.
   Proof.
     iIntros (<-<-???) "(#Hinv & Hj & Hl)"; subst.
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
+    iDestruct "Hinv" as (ρ) "Hinv".
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid.
@@ -269,14 +277,15 @@ Section rules.
     rewrite bool_decide_true //.
   Qed.
 
-  Lemma step_faa E ρ j K l e1 e2 (i1 i2 : Z) :
+  Lemma step_faa E j K l e1 e2 (i1 i2 : Z) :
     IntoVal e1 #i2 →
     nclose specN ⊆ E →
-    spec_ctx ρ ∗ j ⤇ fill K (FAA #l e1) ∗ l ↦ₛ #i1
+    spec_ctx ∗ j ⤇ fill K (FAA #l e1) ∗ l ↦ₛ #i1
     ={E}=∗ j ⤇ fill K #i1 ∗ l ↦ₛ #(i1+i2).
   Proof.
     iIntros (<-?) "(#Hinv & Hj & Hl)"; subst.
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
+    iDestruct "Hinv" as (ρ) "Hinv".
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid.
@@ -296,12 +305,13 @@ Section rules.
   Qed.
 
   (** Fork *)
-  Lemma step_fork E ρ j K e :
+  Lemma step_fork E j K e :
     nclose specN ⊆ E →
-    spec_ctx ρ ∗ j ⤇ fill K (Fork e) ={E}=∗ ∃ j', j ⤇ fill K #() ∗ j' ⤇ e.
+    spec_ctx ∗ j ⤇ fill K (Fork e) ={E}=∗ ∃ j', j ⤇ fill K #() ∗ j' ⤇ e.
   Proof.
     iIntros (?) "[#Hspec Hj]".
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
+    iDestruct "Hspec" as (ρ) "Hspec".
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid.
diff --git a/theories/tests/tp_tests.v b/theories/tests/tp_tests.v
index 9213530f4aa0aa7d03a3af8192b89605b9f4a06d..62204210d4444361e031bc8733d5079cdae6f9a5 100644
--- a/theories/tests/tp_tests.v
+++ b/theories/tests/tp_tests.v
@@ -7,9 +7,9 @@ Section test.
 Context `{relocG Σ}.
 
 (* store, load, and some pure reductions *)
-Lemma test1 E1 j K (l : loc) (n : nat) ρ :
+Lemma test1 E1 j K (l : loc) (n : nat) :
   nclose specN ⊆ E1 →
-  spec_ctx ρ -∗
+  spec_ctx -∗
   j ⤇ fill K ((λ: "x", #l <- "x" + #1) !#l)%E -∗
   l ↦ₛ #n
   ={E1}=∗ l ↦ₛ #(n+1) ∗ j ⤇ fill K #().
@@ -23,9 +23,9 @@ Proof.
 Qed.
 
 (* CAS *)
-Lemma test2 E1 j K (l : loc) (n : nat) ρ :
+Lemma test2 E1 j K (l : loc) (n : nat) :
   nclose specN ⊆ E1 →
-  spec_ctx ρ -∗
+  spec_ctx -∗
   j ⤇ fill K (CAS #l #2 #n;; CAS #l #3 (#n*#2)) -∗
   l ↦ₛ #3
   ={E1}=∗ l ↦ₛ #(n*2) ∗ j ⤇ fill K #true.
@@ -40,21 +40,20 @@ Proof.
 Qed.
 
 (* fork *)
-Lemma test3 E1 j e K (l : loc) (n : nat) ρ :
+Lemma test3 E1 j e K (l : loc) (n : nat) :
   nclose specN ⊆ E1 →
-  spec_ctx ρ -∗
+  spec_ctx -∗
   j ⤇ fill K (Fork e)
   ={E1}=∗ ∃ i, i ⤇ e ∗ j ⤇ fill K #().
 Proof.
   iIntros (?) "#? Hj".
-  tp_fork j. Undo.
   tp_fork j as i. eauto with iFrame.
 Qed.
 
 (* alloc *)
-Lemma test4 E1 j K (n : nat) ρ :
+Lemma test4 E1 j K (n : nat) :
   nclose specN ⊆ E1 →
-  spec_ctx ρ -∗
+  spec_ctx -∗
   j ⤇ fill K (ref #3)
   ={E1}=∗ ∃ l, l ↦ₛ #3 ∗ j ⤇ fill K #l.
 Proof.
@@ -71,12 +70,12 @@ End test.
 (* (* TODO: Coq complains if I make it a section variable *) *)
 (* Axiom (steps_release_test : forall E ρ j K (l : loc) (b : bool), *)
 (*     nclose specN ⊆ E → *)
-(*     spec_ctx ρ -∗ l ↦ₛ #b -∗ j ⤇ fill K (App #() #l) *)
+(*     spec_ctx -∗ l ↦ₛ #b -∗ j ⤇ fill K (App #() #l) *)
 (*     ={E}=∗ j ⤇ fill K #() ∗ l ↦ₛ #false). *)
 
 (* Theorem test_apply E ρ j (b : bool) K l: *)
 (*   nclose specN ⊆ E → *)
-(*   spec_ctx ρ -∗  *)
+(*   spec_ctx -∗  *)
 (*   l ↦ₛ #b -∗ j ⤇ fill K (App #() #l) *)
 (*   -∗ |={E}=> True. *)
 (* Proof. *)
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 430ac9f2e638e06f6942b647a308dd1f5e790fbd..27e88df6b850cd4d2b253fc69f543f37f8c7376c 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -102,7 +102,7 @@ Section fundamental.
     iApply refines_arrow_val.
     iModIntro. iLöb as "IH". iIntros (v1 v2) "#Hτ1".
     rel_pure_l. rel_pure_r.
-    iApply refines_spec_ctx. iDestruct 1 as (ρ) "#Hs".
+    iApply refines_spec_ctx. iIntros "#Hs".
 
     set (r := (RecV f x (subst_map (binder_delete x (binder_delete f (fst <$> vs))) e), RecV f x (subst_map (binder_delete x (binder_delete f (snd <$> vs))) e'))).
     set (vvs' := binder_insert f r (binder_insert x (v1,v2) vs)).