diff --git a/_CoqProject b/_CoqProject
index 8cc2e1a3b7f4b63962c34fb47a5bfe9a77d4f806..b4749740542cd68c1cf71c14c2df947590c0e760 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -55,11 +55,11 @@ theories/examples/lateearlychoice.v
 theories/examples/coinflip.v
 
 theories/examples/par.v
-
 theories/experimental/cka.v
 
 theories/experimental/helping/offers.v
 theories/experimental/helping/helping_stack.v
+theories/experimental/helping/helping_wrapper.v
 
 theories/experimental/hocap/counter.v
 theories/experimental/hocap/ticket_lock.v
diff --git a/theories/examples/or.v b/theories/examples/or.v
index 00ed7125c417c8931d67ce380222195bbeb6b968..510698a3faef48285135d9c9195a1d9dca73de74 100644
--- a/theories/examples/or.v
+++ b/theories/examples/or.v
@@ -30,7 +30,8 @@ Notation "e1 âŠ• e2" := (or (Î»: <>, e1)%V (Î»: <>, e2)%V)
                         (at level 60) : val_scope.
 
 Section rules.
-  Context `{relocG Î£}.
+  Context `{!relocG Î£}.
+  Implicit Types e : expr.
 
   (** Symbolic execution rule for the LHS *)
   Definition or_inv x : iProp Î£ :=
diff --git a/theories/examples/par.v b/theories/examples/par.v
index 7040f745b7549509f44ccf335c513d0ac992b720..587f2560af40b1a09c91701b80533f5fd0cd177e 100644
--- a/theories/examples/par.v
+++ b/theories/examples/par.v
@@ -24,6 +24,7 @@ Notation "e1 âˆ¥ e2" := (((e1;; #()) ||| (e2;; #()));; #())%E
 
 Section rules.
   Context `{!relocG Î£, !spawnG Î£}.
+  Implicit Type e t : expr.
 
   Lemma par_l_2 e1 e2 t :
     (WP e1 {{ _, True }}) -âˆ—
@@ -85,20 +86,26 @@ Section rules.
     rel_pures_l. rel_rec_l.
     rel_pures_l.
     pose (N:=nroot.@"par").
-    rewrite refines_eq /refines_def. iIntros (j K) "#Hspec Hj".
-    iModIntro. wp_bind (spawn _).
-    iApply (spawn_spec N (Î» _, j â¤‡ fill K #())%I with "[He1 Hj]").
+    iApply refines_split. iIntros (k) "Hk".
+    rel_bind_l (spawn _). iApply refines_wp_l.
+    iApply (spawn_spec N (Î» _, refines_right k #())%I with "[He1 Hk]").
     - wp_pures. wp_bind e1.
-      iMod ("He1" with "Hspec Hj") as "He1".
+      rewrite refines_eq /refines_def.
+      iDestruct "Hk" as "[#Hs Hj]".
+      iMod ("He1" with "[$Hs $Hj]") as "He1".
       iApply (wp_wand with "He1").
       iIntros (?)  "P". wp_pures.
-      by iDestruct "P" as (v') "[Hj [-> ->]]".
+      iFrame "Hs".
+      by iDestruct "P" as (v') "[? [-> ->]]".
     - iNext. iIntros (l) "hndl". iSimpl.
-      wp_pures. wp_bind e2.
+      rel_pures_l. rel_bind_l e2.
+      iApply refines_wp_l.
       iApply (wp_wand with "He2"). iIntros (?) "_".
-      wp_pures.
-      wp_apply (join_spec with "hndl").
-      iIntros (?) "Hj". wp_pures. iExists #(). eauto with iFrame.
+      simpl. rel_pures_l. rel_bind_l (spawn.join _).
+      iApply refines_wp_l.
+      iApply (join_spec with "hndl"). iNext.
+      iIntros (?) "Hk". simpl. rel_pures_l. iApply (refines_combine with "[] Hk").
+      rel_values.
   Qed.
 
   Lemma par_l_1' Q K e1 e2 t :
@@ -111,27 +118,30 @@ Section rules.
     rel_pures_l. rel_rec_l.
     rel_pures_l.
     pose (N:=nroot.@"par").
-    rewrite {1 3}refines_eq /refines_def. iIntros (j K') "#Hspec Hj".
-    iModIntro. wp_bind (spawn _).
-    iApply (spawn_spec N (Î» _, j â¤‡ fill (K++K') #())%I with "[He1 Hj]").
+    iApply refines_split. iIntros (k) "Hk".
+    rel_bind_l (spawn _). iApply refines_wp_l.
+    rewrite refines_right_bind.
+    iApply (spawn_spec N (Î» _, refines_right k (fill K #()))%I with "[He1 Hk]").
     - wp_pures. wp_bind e1.
-      rewrite -fill_app.
-      iMod ("He1" with "Hspec Hj") as "He1".
+      rewrite refines_eq /refines_def.
+      iAssert (spec_ctx) with "[Hk]" as "#Hs".
+      { iDestruct "Hk" as "[$ _]". }
+      iMod ("He1" with "Hk") as "He1".
       iApply (wp_wand with "He1").
       iIntros (?)  "P". wp_pures.
-      by iDestruct "P" as (v') "[Hj [-> ->]]".
-    - iNext. iIntros (l) "hndl". iSimpl.
-      wp_pures. wp_bind e2.
+      rewrite /refines_right.
+      iDestruct "P" as (v') "[Hj [-> ->]]".
+      iFrame "Hs". by rewrite fill_app.
+    - iNext. iIntros (l) "Hl". simpl.
+      rel_pures_l. rel_bind_l e2.
+      iApply refines_wp_l.
       iApply (wp_wand with "He2"). iIntros (?) "HQ".
-      wp_pures.
-      wp_apply (join_spec with "hndl").
-      iIntros (?) "Hj".
-      iSpecialize ("Ht" with "HQ").
-      rewrite refines_eq /refines_def.
-      rewrite fill_app.
-      iMod ("Ht" with "Hspec Hj") as "Ht".
-      rewrite wp_value_fupd. iMod "Ht" as (?) "[Ht [_ ->]]".
-      wp_pures. iExists #(). eauto with iFrame.
+      simpl. rel_pures_l. rel_bind_l (spawn.join _).
+      iApply refines_wp_l.
+      wp_apply (join_spec with "Hl").
+      iIntros (?) "Hk".
+      iSpecialize ("Ht" with "HQ"). simpl.
+      rel_pures_l. iApply (refines_combine with "Ht Hk").
   Qed.
 
   (* Lemma par_r_1 e1 e2 t (A : lrel Î£) E : *)
@@ -202,14 +212,17 @@ Section rules.
     tp_pure i (App _ _). simpl.
     rel_pures_r.
     rel_bind_r e2.
-    iApply refines_spec_ctx. iIntros "#Hs".
-    iApply (par_l_1' (i â¤‡ (#c2 <- InjR (#();; #())))%I
+    iApply (par_l_1' (refines_right i (#c2 <- InjR (#();; #())))%I
               with "He2 [He1 Hi]").
     { rewrite refines_eq /refines_def.
       tp_bind i e1.
-      iMod ("He1" with "Hs Hi") as "He1". simpl.
+      rewrite refines_right_bind.
+      iAssert (spec_ctx) with "[Hi]" as "#Hs".
+      { iDestruct "Hi" as "[$ _]". }
+      iMod ("He1" with "Hi") as "He1". simpl.
       iApply (wp_wand with "He1"). iIntros (?).
-      iDestruct 1 as (?) "[Hi [-> ->]]". done. }
+      iDestruct 1 as (?) "[Hi [-> ->]]".
+      rewrite /refines_right. by iFrame. }
     iIntros "Hi". simpl. rel_pures_r.
     tp_pures i. tp_store i.
     rel_rec_r. rel_load_r. rel_pures_r. rel_values.
@@ -242,28 +255,39 @@ Section rules.
     { simpl. eauto. }
     repeat rel_pure_r.
     tp_rec i. simpl.
-    rewrite {3}refines_eq /refines_def.
-    iIntros (j K) "#Hs Hj". iModIntro.
+    rewrite {3}refines_eq /refines_def /=.
+    iIntros (j' K).
+    set (j := {| tp_id := j'; tp_ctx := K |}).
+    iIntros "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 "Hs Hi") as "He1".
+    iDestruct "Hi" as "[#Hs Hi]".
+    iMod ("He1" $! (tp_id i)  with "[Hi]") as "He1".
+    { rewrite /refines_right -fill_app //. by iFrame. }
     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 "Hs Hj") as "He2".
+    iMod ("He2" $! (tp_id j) with "[Hj]") as "He2".
+    { rewrite /refines_right -fill_app //.
+      cbn-[fill]. iFrame "Hj". }
     iApply wp_fupd.
     iApply (wp_wand with "He2"). iIntros (w1).
     iDestruct 1 as (w2) "[Hj Hw]".
     iSimpl in "Hi". iSimpl in "Hj".
+    iAssert (refines_right i (#c2 <- InjR v2)) with "[$Hi]" as "Hi".
+    { by iFrame. }
+    iAssert (refines_right j (let: "v2" := w2 in let: "v1" := spawn.join #c2 in ("v1", "v2"))) with "[Hj]" as "Hj".
+    { by iFrame. }
     tp_pure i _.
     tp_store i.
     tp_pures j. tp_rec j.
     tp_load j.
     tp_pures j.
-    iModIntro. iExists _. iFrame.
+    iModIntro. iExists _.
+    iDestruct "Hj" as "[_ $]".
   Qed.
 
   Lemma interchange a b c d (A B C D : lrel Î£) :
@@ -286,45 +310,68 @@ Section rules.
     tp_rec i. simpl.
     rel_rec_l. repeat rel_pure_l.
     rewrite {5}refines_eq /refines_def.
-    iIntros (j K) "#Hs Hj". iModIntro.
+    iIntros (j' K). simpl.
+    set (j := {| tp_id := j'; tp_ctx := K |}).
     pose (N:=nroot.@"par").
+    iIntros "Hj". iModIntro.
     wp_bind (spawn _).
     iApply (spawn_spec N with "[Ha Hj]").
     - wp_lam. rewrite refines_eq /refines_def.
       tp_bind j a.
-      iMod ("Ha" with "Hs Hj") as "Ha".
+      iMod ("Ha" with "[Hj]") as "Ha".
+      { rewrite /refines_right -fill_app //.
+        cbn-[fill]. iFrame "Hj". }
       iExact "Ha".
     - iNext. iIntros (h) "Hdl". wp_pures.
       wp_bind b.
       rewrite {1}refines_eq /refines_def.
       tp_bind i b.
-      iMod ("Hb" with "Hs Hi") as "Hb".
+      iDestruct "Hi" as "[#Hs Hi]".
+      iMod ("Hb" with "[Hi]") as "Hb".
+      { rewrite /refines_right -fill_app //; by iFrame. }
       iApply (wp_wand with "Hb").
       iIntros (bv). iDestruct 1 as (bv') "[Hi HB]". simpl.
       wp_pures. wp_bind (spawn.join _).
       iApply (join_spec with "Hdl").
       iNext. iIntros (av). iDestruct 1 as (av') "[Hj HA]".
-      wp_pures. tp_pures j. tp_pures i.
+      wp_pures.
+      iAssert (refines_right i (#c2 <- InjR (bv';; c))) with "[Hi]" as "Hi".
+      { by iFrame. }
+      iAssert (refines_right j (let: "v2" := av';; d in
+              let: "v1" := spawn.join #c2 in ("v1", "v2")))
+        with "[Hj]" as "Hj".
+      { by iFrame. }
+      tp_pures j. tp_pures i.
       wp_rec. wp_pures.
       wp_apply (spawn_spec N with "[Hc Hi]").
       { wp_pures.
-        rewrite refines_eq /refines_def.
+        rewrite refines_eq /refines_def /=.
         tp_bind i c.
-        iMod ("Hc" with "Hs Hi") as "Hc". iExact "Hc". }
+        iMod ("Hc" with "[Hi]") as "Hc".
+        { rewrite /refines_right -fill_app //. }
+        iExact "Hc". }
       clear h. iIntros (h) "Hdl". wp_pures.
       wp_bind d.
       rewrite refines_eq /refines_def.
       tp_bind j d.
-      iMod ("Hd" with "Hs Hj") as "Hd".
+      iMod ("Hd" $! (tp_id j) with "[Hj]") as "Hd".
+      { rewrite /refines_right -fill_app //.
+        iSimpl. by iFrame. }
       iApply (wp_wand with "Hd"). iIntros (dv).
       iDestruct 1 as (dv') "[Hj HD]".
       wp_pures. wp_apply (join_spec with "Hdl").
       iIntros (cv). iDestruct 1 as (cv') "[Hi HC]".
       iApply wp_fupd.
       wp_pures. iExists (cv', dv')%V. simpl.
+      iAssert (refines_right i (#c2 <- InjR cv')) with "[Hi]" as "Hi".
+      { by iFrame. }
+      iAssert (refines_right j (let: "v2" := dv' in let: "v1" := spawn.join #c2 in ("v1", "v2"))) with "[Hj]" as "Hj".
+      { by iFrame. }
       tp_pures i. tp_store i.
       tp_pures j.
       rewrite /spawn.join. tp_pures j.
-      tp_load j. tp_pures j. eauto with iFrame.
+      tp_load j. tp_pures j.
+      iModIntro; iSplit; eauto with iFrame.
+      iDestruct "Hj" as "[_ $]".
   Qed.
 End rules.
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index 4a65ea21ed887f751a5b97fa67dc5b0d41c18a09..ae23fda3363419cc361c816dffa7e5f753d7fa5a 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -21,7 +21,7 @@ Class tlockG Î£ :=
   tlock_G :> inG Î£ (authR (gset_disjUR nat)).
 Definition tlockÎ£ : gFunctors :=
   #[ GFunctor (authR $ gset_disjUR nat) ].
-Instance subG_tlockÎ£ {Î£} : subG tlockÎ£ Î£ â†’ tlockG Î£.
+Global Instance subG_tlockÎ£ {Î£} : subG tlockÎ£ Î£ â†’ tlockG Î£.
 Proof. solve_inG. Qed.
 
 Definition lockPool := gset ((loc * loc * gname) * loc).
@@ -30,7 +30,7 @@ Definition lockPoolR := gsetUR ((loc * loc * gname) * loc).
 Class lockPoolG Î£ :=
   lockPool_inG :> inG Î£ (authR lockPoolR).
 Definition lockPoolÎ£ := #[ GFunctor (authR $ lockPoolR) ].
-Instance subG_lockPoolÎ£ {Î£} : subG lockPoolÎ£ Î£ â†’ lockPoolG Î£.
+Global Instance subG_lockPoolÎ£ {Î£} : subG lockPoolÎ£ Î£ â†’ lockPoolG Î£.
 Proof. solve_inG. Qed.
 
 Section refinement.
@@ -69,9 +69,9 @@ Section refinement.
     by iFrame.
   Qed.
 
-  Instance ticket_timeless Î³ n : Timeless (ticket Î³ n).
+  Global Instance ticket_timeless Î³ n : Timeless (ticket Î³ n).
   Proof. apply _. Qed.
-  Instance issuedTickets_timeless Î³ n : Timeless (issuedTickets Î³ n).
+  Global Instance issuedTickets_timeless Î³ n : Timeless (issuedTickets Î³ n).
   Proof. apply _. Qed.
 
   Opaque ticket issuedTickets.
@@ -82,7 +82,7 @@ Section refinement.
    âˆ— issuedTickets Î³ n âˆ— is_locked_r l' b
    âˆ— if b then ticket Î³ o else True)%I.
 
-  Instance ifticket_timeless (b : bool) Î³ o :
+  Local Instance ifticket_timeless (b : bool) Î³ o :
     Timeless (if b then ticket Î³ o else True)%I.
   Proof. destruct b; apply _. Qed.
   Instance lockInv_timeless lo ln Î³ l' : Timeless (lockInv lo ln Î³ l').
diff --git a/theories/examples/various.v b/theories/examples/various.v
index 0ba447068ee8d72d85211fc4cd3596a712799caa..48db6e77209d1f3df3c08b79b78cea3dd04da5af 100644
--- a/theories/examples/various.v
+++ b/theories/examples/various.v
@@ -14,7 +14,7 @@ Instance subG_oneshotÎ£ {Î£} : subG oneshotÎ£ Î£ â†’ oneshotG Î£.
 Proof. solve_inG. Qed.
 
 Section proofs.
-  Context `{relocG Î£}.
+  Context `{!relocG Î£}.
 
   Lemma refinement1 :
     âŠ¢ REL
@@ -366,7 +366,7 @@ Section proofs.
      (c1 â†¦ #n âˆ— c2 â†¦â‚› #n âˆ— pending Î³)
    âˆ¨ (c1 â†¦ #(n+1) âˆ— c2 â†¦â‚› #n âˆ— shot Î³ âˆ— own Î³' (Excl ())))%I.
 
-  Lemma profiled_g `{oneshotG Î£} `{inG Î£ (exclR unitR)} Î³ Î³' c1 c2 g1 g2 :
+  Lemma profiled_g `{oneshotG Î£} `{inG Î£ (exclR unitR)} Î³ Î³' c1 c2 (g1 g2 : expr) :
     inv shootN (i6 c1 c2 Î³ Î³') -âˆ—
     â–¡ (REL g1 << g2 : () â†’ ()) -âˆ—
     REL
@@ -440,7 +440,8 @@ Section proofs.
           rel_values. }
   Qed.
 
-  Lemma profiled_g' `{oneshotG Î£} `{inG Î£ (exclR unitR)} Î³ Î³' c1 c2 g1 g2 :
+  Lemma profiled_g' `{!oneshotG Î£} `{!inG Î£ (exclR unitR)}
+        Î³ Î³' c1 c2 (g1 g2 : expr) :
     inv shootN (i6 c1 c2 Î³ Î³') -âˆ—
     â–¡ (REL g1 << g2 : () â†’ ()) -âˆ—
     REL
@@ -469,7 +470,8 @@ Section proofs.
     iFrame.
   Qed.
 
-  Lemma refinement6_helper f'1 f'2 g1 g2 c1 c2 Î³ Î³' m `{oneshotG Î£} `{inG Î£ (exclR unitR)} :
+  Lemma refinement6_helper (f'1 f'2 g1 g2 : expr)
+        c1 c2 Î³ Î³' m `{oneshotG Î£} `{inG Î£ (exclR unitR)} :
     inv shootN (i6 c1 c2 Î³ Î³') -âˆ—
     â–¡ (REL g1 << g2 : () â†’ ()) -âˆ—
     â–¡ (REL f'1 << f'2 : (() â†’ ()) â†’ ()) -âˆ—
diff --git a/theories/experimental/cka.v b/theories/experimental/cka.v
index 9f83118a77d2fc54810269b305aa36a8689d0dd6..ad33e36cfa116347bd9ee6bf0d276cc06deb3ecb 100644
--- a/theories/experimental/cka.v
+++ b/theories/experimental/cka.v
@@ -174,7 +174,9 @@ Definition star : val := rec: "star" "f" :=
 Notation "e **" := (star (Î»: <>, e)%V) (at level 80).
 
 Section rules.
-  Context `{relocG Î£}.
+  Context `{!relocG Î£}.
+
+  Implicit Types e : expr.
 
   Lemma star_compatible e e' :
     â–¡ (REL e << e' : ()) -âˆ—
@@ -188,15 +190,6 @@ Section rules.
     - iApply "IH".
   Qed.
 
-  (* Lemma star_refines_l e t : *)
-  (*   REL e ** << t : (). *)
-  (* Proof. *)
-  (*   iIntros "H". rel_rec_l. repeat rel_pure_l. *)
-  (*   iApply or_compatible; first by rel_values. *)
-  (*   iApply refines_seq. *)
-  (*   - rel_pure_l. rel_pure_r. iAssumption. *)
-  (*   - iApply "IH". *)
-
   Lemma star_id_1 e e' :
     â–¡(REL e << e' : ()) -âˆ—
     REL e ** << (#() âŠ• (e';; e' **))%V : ().
diff --git a/theories/experimental/helping/helping_stack.v b/theories/experimental/helping/helping_stack.v
index d160868c16fd5cca0d9df0b9e6fe99fbe74f3d33..b942ab5544bbb2635e33d3d30d44a68c52c50dd4 100644
--- a/theories/experimental/helping/helping_stack.v
+++ b/theories/experimental/helping/helping_stack.v
@@ -82,19 +82,18 @@ Definition CG_mkstack : val := Î»: <>,
 value that is being offered and a potential thread with the
 continuation that accepts the offer, if it is present. *)
 
-Canonical Structure ectx_itemO := leibnizO ectx_item.
-Definition offerReg := gmap loc (val * gname * nat * (list ectx_item)).
+Definition offerReg := gmap loc (val * gname * ref_id).
 Definition offerRegR :=
-  gmapUR loc (agreeR (prodO valO (prodO gnameO (prodO natO (listO ectx_itemO))))).
+  gmapUR loc (agreeR (prodO valO (prodO gnameO ref_idO))).
 
 Class offerRegPreG Î£ := OfferRegPreG {
   offerReg_inG :> inG Î£ (authR offerRegR)
 }.
 
-Definition offerize (x : (val * gname * nat * (list ectx_item))) :
-  (agreeR (prodO valO (prodO gnameO (prodO natO (listO ectx_itemO))))) :=
+Definition offerize (x : (val * gname * ref_id)) :
+  (agreeR (prodO valO (prodO gnameO ref_idO))) :=
   match x with
-  | (v, Î³, n, K) => to_agree (v, (Î³, (n, K)))
+  | (v, Î³, k) => to_agree (v, (Î³, k))
   end.
 
 Definition to_offer_reg : offerReg -> offerRegR := fmap offerize.
@@ -102,32 +101,32 @@ Definition to_offer_reg : offerReg -> offerRegR := fmap offerize.
 Lemma to_offer_reg_valid N : âœ“ to_offer_reg N.
 Proof.
   intros l. rewrite lookup_fmap. case (N !! l); simpl; try done.
-  intros [[[v Î³] n] K]; simpl. done.
+  intros [[v Î³] k]; simpl. done.
 Qed.
 
 Section offerReg_rules.
   Context `{!offerRegPreG Î£, !offerG Î£}.
 
   Lemma offerReg_alloc (o : loc) (v : val) (Î³ : gname)
-    (j : nat) (K : list ectx_item) (Î³o : gname) (N : offerReg)  :
+    (k : ref_id) (Î³o : gname) (N : offerReg)  :
     N !! o = None â†’
     own Î³o (â— to_offer_reg N)
-    ==âˆ— own Î³o (â— to_offer_reg (<[o:=(v, Î³, j, K)]> N))
-      âˆ— own Î³o (â—¯ {[o := offerize (v, Î³, j, K)]}).
+    ==âˆ— own Î³o (â— to_offer_reg (<[o:=(v, Î³, k)]> N))
+      âˆ— own Î³o (â—¯ {[o := offerize (v, Î³, k)]}).
   Proof.
     iIntros (HNo) "HN".
     iMod (own_update with "HN") as "[HN Hfrag]".
     { eapply auth_update_alloc.
-      eapply (alloc_singleton_local_update _ o (to_agree (v, (Î³, (j, K))))); try done.
+      eapply (alloc_singleton_local_update _ o (to_agree (v, (Î³, k)))); try done.
       by rewrite /to_offer_reg lookup_fmap HNo. }
     iFrame. by rewrite /to_offer_reg fmap_insert.
   Qed.
 
   Lemma offerReg_frag_lookup (o : loc) (v : val) (Î³ : gname)
-    (j : nat) (K : list ectx_item) (Î³o : gname) (N : offerReg)  :
+    k (Î³o : gname) (N : offerReg)  :
     own Î³o (â— to_offer_reg N)
-    -âˆ— own Î³o (â—¯ {[o := to_agree (v, (Î³, (j, K)))]})
-    -âˆ— âŒœN !! o = Some (v, Î³, j, K)âŒ.
+    -âˆ— own Î³o (â—¯ {[o := to_agree (v, (Î³, k))]})
+    -âˆ— âŒœN !! o = Some (v, Î³, k)âŒ.
   Proof.
     iIntros "HN Hfrag".
     iDestruct (own_valid_2 with "HN Hfrag") as %Hfoo.
@@ -146,23 +145,23 @@ Section offerReg_rules.
     intros Hav.
     rewrite -(inj Some _ _ Hav).
     rewrite Some_included_total.
-    destruct av' as [[[??]?]?]. simpl.
+    destruct av' as [[??]?]. simpl.
     rewrite to_agree_included.
     fold_leibniz.
     intros. by simplify_eq.
   Qed.
 
   Lemma offerReg_lookup_frag (o : loc) (v : val) (Î³ : gname)
-    (j : nat) (K : list ectx_item) (Î³o : gname) (N : offerReg) :
-    N !! o = Some (v, Î³, j, K) â†’
+    (k : ref_id) (Î³o : gname) (N : offerReg) :
+    N !! o = Some (v, Î³, k) â†’
     own Î³o (â— to_offer_reg N)
-    ==âˆ— own Î³o (â—¯ {[o := to_agree (v, (Î³, (j, K)))]})
+    ==âˆ— own Î³o (â—¯ {[o := to_agree (v, (Î³, k))]})
       âˆ— own Î³o (â— to_offer_reg N).
   Proof.
     iIntros (HNo) "Hown".
     iMod (own_update with "[Hown]") as "Hown".
     { eapply (auth_update (to_offer_reg N) âˆ…).
-      eapply (op_local_update_discrete _ âˆ… {[o := to_agree (v, (Î³, (j, K)))]}).
+      eapply (op_local_update_discrete _ âˆ… {[o := to_agree (v, (Î³, k))]}).
       intros. intros i. destruct (decide (i = o)); subst; rewrite lookup_op.
       + rewrite lookup_singleton lookup_fmap HNo.
         rewrite -Some_op.
@@ -178,7 +177,7 @@ Section offerReg_rules.
       rewrite right_id. iFrame "Hown". }
     iDestruct "Hown" as "[Ho Hown]".
     rewrite right_id. iFrame.
-    assert ({[o := to_agree (v, (Î³, (j, K)))]} â‹… to_offer_reg N â‰¡ to_offer_reg N) as Hfoo.
+    assert ({[o := to_agree (v, (Î³, k))]} â‹… to_offer_reg N â‰¡ to_offer_reg N) as Hfoo.
     { intro i.
       rewrite /to_offer_reg lookup_merge !lookup_fmap.
       destruct (decide (i = o)); subst.
@@ -196,9 +195,9 @@ Section offerReg_rules.
   Definition offerInv `{!relocG Î£} (N : offerReg) (st' : val) : iProp Î£ :=
     ([âˆ— map] l â†¦ w âˆˆ N,
      match w with
-     | (v,Î³,j,K) => is_offer Î³ l
-                             (j â¤‡ fill K (CG_locked_push st' (of_val v))%E)
-                             (j â¤‡ fill K #())
+     | (v,Î³,k) => is_offer Î³ l
+                             (refines_right k (CG_locked_push st' (of_val v))%E)
+                             (refines_right k #())
      end)%I.
 
   Lemma offerInv_empty `{!relocG Î£} (st' : val) : âŠ¢ offerInv âˆ… st'.
@@ -210,7 +209,7 @@ Section offerReg_rules.
     rewrite /offerInv. iIntros "HN Ho".
     iAssert (âŒœis_Some (N !! o)âŒ â†’ False)%I as %Hbaz.
     {
-      iIntros ([[[[? ?] ?] ?] HNo]).
+      iIntros ([[[? ?] ?] HNo]).
       rewrite (big_sepM_lookup _ N o _ HNo).
       iApply (is_offer_exclusive with "HN Ho").
     }
@@ -251,25 +250,27 @@ Section refinement.
       This is also the only place where we need to unfold the definition of the refinement proposition. *)
   Lemma revoke_offer_l Î³ off E K (v : val) e1 e2 A :
     offer_token Î³ -âˆ—
-    (âˆ€ j K', (j â¤‡ fill K' e1)  ={E}[âŠ¤]â–·=âˆ—
-      â–· is_offer Î³ off (j â¤‡ fill K' e1) (j â¤‡ fill K' e2) âˆ—
-      â–· (is_offer Î³ off (j â¤‡ fill K' e1) (j â¤‡ fill K' e2) -âˆ—
+    (âˆ€ k, refines_right k e1  ={E}[âŠ¤]â–·=âˆ—
+      â–· is_offer Î³ off (refines_right k e1) (refines_right k e2) âˆ—
+      â–· (is_offer Î³ off (refines_right k e1) (refines_right k e2) -âˆ—
            ((REL fill K (of_val NONEV) << e2 @ E : A)
          âˆ§ (REL fill K (of_val $ SOMEV v) << e1 @ E : A)))) -âˆ—
     REL fill K (revoke_offer (v, #off)%V) << e1 @ E : A.
   Proof.
     iIntros "HÎ³ Hlog".
-    rewrite {3}refines_eq /refines_def.
-    iIntros (j K') "#Hs Hj".
-    iMod ("Hlog" with "Hj") as "Hlog".
-    iModIntro. iApply wp_bind. (* TODO: why do we have to use wp_bind here? *)
+    iApply refines_split.
+    iIntros (k) "Hk".
+    iMod ("Hlog" with "Hk") as "Hlog".
+    iApply refines_wp_l.
     wp_apply (wp_revoke_offer with "HÎ³ [-]").
     iNext. iMod "Hlog" as "[Hoff Hcont]". iModIntro.
     iFrame "Hoff". iNext. iSplit.
     - iIntros "Hoff". iDestruct ("Hcont" with "Hoff") as "[Hcont _]".
-      rewrite refines_eq. by iApply "Hcont".
+      iIntros "Hk". iApply refines_left_fupd.
+      iApply (refines_combine with "Hcont Hk").
     - iIntros "Hoff". iDestruct ("Hcont" with "Hoff") as "[_ Hcont]".
-      rewrite refines_eq. by iApply "Hcont".
+      iIntros "Hk". iApply refines_left_fupd.
+      iApply (refines_combine with "Hcont Hk").
   Qed.
 
   (** Then we have definitions and lemmas that we use for actually
@@ -320,10 +321,10 @@ Section refinement.
      âˆ— is_stack st' ls2
      âˆ— ([âˆ— list] v1;v2 âˆˆ ls1;ls2, A v1 v2)
      âˆ— (mb â†¦ NONEV      (* the mailbox is either empty or contains an offer that is in the registry *)
-        âˆ¨ (âˆƒ (l : loc) v1 v2 Î³ j K,
+        âˆ¨ (âˆƒ (l : loc) v1 v2 Î³ k,
               A v1 v2
             âˆ— mb â†¦ SOMEV (v1, #l)
-            âˆ— âŒœN !! l = Some (v2, Î³, j, K)âŒ))
+            âˆ— âŒœN !! l = Some (v2, Î³, k)âŒ))
      âˆ— own oname (â— to_offer_reg N)
      âˆ— offerInv N st')%I.
 
@@ -403,7 +404,7 @@ Section refinement.
       { iNext. iExists _, _, _, _; by iFrame. }
       iApply (pop_no_helping_refinement with "Hinv IH").
     - (* YES OFFER *)
-      iDestruct "Hmb" as (l v1 v2 Î³ j K) "(#Hv & Hmb & >HNl)".
+      iDestruct "Hmb" as (l v1 v2 Î³ k) "(#Hv & >Hmb & >HNl)".
       iDestruct "HNl" as %HNl.
       rewrite /offerInv big_sepM_lookup_acc; eauto. iSimpl in "HN".
       iDestruct "HN" as "[HNl HN]".
@@ -414,7 +415,7 @@ Section refinement.
       iMod ("Hcl" with "[-Hlown IH]") as "_".
       { iNext. iExists _, _, _, _; iFrame.
         iSplitL "Hmb".
-        - iRight. iExists _, _, _, _, _, _.
+        - iRight. iExists _, _, _, _, _.
           eauto with iFrame.
         - by iApply "HN". }
 
@@ -434,22 +435,18 @@ Section refinement.
         rel_pures_l.
         iApply (pop_no_helping_refinement with "Hinv IH").
       + (* An offer was accepted *)
-        iIntros "Hj Hoff". rel_pures_l.
+        iIntros "Hk Hoff". rel_pures_l.
         iDestruct "Hst2" as (st2l lk ->) "[Hlk Hst2]".
-        tp_rec j. tp_pures j. tp_rec j.
+        tp_rec k. tp_pures k. tp_rec k.
         unlock is_locked_r. iDestruct "Hlk" as (lk' ->) "Hl".
         (* TODO: make all the tp_ tactics work without the need for an explicit Fupd *)
-        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.
-        tp_pures j. tp_rec j. tp_pures j.
-        tp_load j. tp_pures j.
-        tp_store j. tp_pures j.
-        tp_rec j. tp_store j.
-        iSpecialize ("Hoff" with "Hj").
+        tp_cmpxchg_suc k.
+        tp_pures k. tp_rec k. tp_pures k.
+        tp_load k. tp_pures k.
+        tp_store k. tp_pures k.
+        tp_rec k. tp_store k.
+        iSpecialize ("Hoff" with "Hk").
         iSpecialize ("HN" with "Hoff").
-        iClear "HÏ". iModIntro.
 
         rel_apply_r (refines_CG_pop_suc_r with "[Hst2 Hl]").
         { iExists st2l,#lk'. rewrite /is_locked_r. by eauto with iFrame. }
@@ -480,20 +477,20 @@ Section refinement.
     iAssert (âˆƒ v, â–· mb â†¦ v)%I with "[Hmb]" as (v) "Hmb".
     { iDestruct "Hmb" as "[Hmb | Hmb]".
       - iExists NONEV; eauto.
-      - iDestruct "Hmb" as (l m1 m2 Î³' j K) "(Hm & Hmb & ?)".
+      - iDestruct "Hmb" as (l m1 m2 Î³' k) "(Hm & Hmb & ?)".
         iExists (SOMEV (m1, #l)); eauto. }
     iExists _; iFrame; iNext.
     iIntros "Hmb".
 
     rel_pures_l.
     rel_apply_l (revoke_offer_l with "Htok").
-    iIntros (j K') "Hj". iSpecialize ("Hoff" with "Hj").
+    iIntros (k) "Hk". iSpecialize ("Hoff" with "Hk").
     iDestruct (offerInv_excl with "HN Hoff") as %?.
-    iMod (offerReg_alloc off h2 Î³ j K' with "HNown") as "[HNown #Hfrag]"; eauto.
+    iMod (offerReg_alloc off h2 Î³ k with "HNown") as "[HNown #Hfrag]"; eauto.
     iMod ("Hcl" with "[-]") as "_".
     { iNext. iExists _,_,_,_; iFrame.
       iSplitL "Hmb".
-      - iRight. iExists off, h1, h2, _, _, _. iFrame "Hmb Hh".
+      - iRight. iExists off, h1, h2, _, _. iFrame "Hmb Hh".
         iPureIntro. by rewrite lookup_insert.
       - rewrite /offerInv big_sepM_insert; eauto with iFrame. }
     iModIntro. iNext.
diff --git a/theories/experimental/helping/helping_wrapper.v b/theories/experimental/helping/helping_wrapper.v
index b197ef2d6da45de0e9030863d557fb379bcacb18..b2c3cde172f733059e2f835e7b96ca5229374c0d 100644
--- a/theories/experimental/helping/helping_wrapper.v
+++ b/theories/experimental/helping/helping_wrapper.v
@@ -9,7 +9,6 @@
     TODO: support recursion/callbacks into the wrapped functions.
  *)
 From iris.algebra Require Import auth gmap agree list excl.
-From iris.base_logic.lib Require Import auth.
 From reloc Require Export reloc experimental.helping.offers.
 From reloc Require Import lib.list.
 
@@ -46,19 +45,29 @@ Definition mk_helping : val := Î»: "new_ds",
   (Î»: <>, wrap_pop "f1" "mb",
    Î»: "x", wrap_push "f2" "mb" "x").
 
+(** * Logical theory of an offer registry *)
+(** We will use an "offer registery". It associates for each offer a
+value that is being offered and a potential thread with the
+continuation that accepts the offer, if it is present. *)
+
 Canonical Structure ectx_itemO := leibnizO ectx_item.
-Definition offerReg := gmap loc (val * gname * nat * (list ectx_item)).
+(* TODO: move !! *)
+Canonical Structure ref_idO := leibnizO ref_id.
+Global Instance ref_id_inhabited : Inhabited ref_id.
+Proof. split. apply (RefId 0 []). Qed.
+
+Definition offerReg := gmap loc (val * gname * ref_id).
 Definition offerRegR :=
-  gmapUR loc (agreeR (prodO valO (prodO gnameO (prodO natO (listO ectx_itemO))))).
+  gmapUR loc (agreeR (prodO valO (prodO gnameO ref_idO))).
 
 Class offerRegPreG Î£ := OfferRegPreG {
-  offerReg_inG :> authG Î£ offerRegR
+  offerReg_inG :> inG Î£ (authUR offerRegR)
 }.
 
-Definition offerize (x : (val * gname * nat * (list ectx_item))) :
-  (agreeR (prodO valO (prodO gnameO (prodO natO (listO ectx_itemO))))) :=
+Definition offerize (x : (val * gname * ref_id)) :
+  (agreeR (prodO valO (prodO gnameO ref_idO))) :=
   match x with
-  | (v, Î³, n, K) => to_agree (v, (Î³, (n, K)))
+  | (v, Î³, k) => to_agree (v, (Î³, k))
   end.
 
 Definition to_offer_reg : offerReg -> offerRegR := fmap offerize.
@@ -66,32 +75,32 @@ Definition to_offer_reg : offerReg -> offerRegR := fmap offerize.
 Lemma to_offer_reg_valid N : âœ“ to_offer_reg N.
 Proof.
   intros l. rewrite lookup_fmap. case (N !! l); simpl; try done.
-  intros [[[v Î³] n] K]; simpl. done.
+  intros [[v Î³] k]; simpl. done.
 Qed.
 
 Section offerReg_rules.
   Context `{!offerRegPreG Î£, !offerG Î£}.
 
   Lemma offerReg_alloc (o : loc) (v : val) (Î³ : gname)
-    (j : nat) (K : list ectx_item) (Î³o : gname) (N : offerReg)  :
+    (k : ref_id) (Î³o : gname) (N : offerReg)  :
     N !! o = None â†’
     own Î³o (â— to_offer_reg N)
-    ==âˆ— own Î³o (â— to_offer_reg (<[o:=(v, Î³, j, K)]> N))
-      âˆ— own Î³o (â—¯ {[o := offerize (v, Î³, j, K)]}).
+    ==âˆ— own Î³o (â— to_offer_reg (<[o:=(v, Î³, k)]> N))
+      âˆ— own Î³o (â—¯ {[o := offerize (v, Î³, k)]}).
   Proof.
     iIntros (HNo) "HN".
     iMod (own_update with "HN") as "[HN Hfrag]".
     { eapply auth_update_alloc.
-      eapply (alloc_singleton_local_update _ o (to_agree (v, (Î³, (j, K))))); try done.
+      eapply (alloc_singleton_local_update _ o (to_agree (v, (Î³, k)))); try done.
       by rewrite /to_offer_reg lookup_fmap HNo. }
     iFrame. by rewrite /to_offer_reg fmap_insert.
   Qed.
 
   Lemma offerReg_frag_lookup (o : loc) (v : val) (Î³ : gname)
-    (j : nat) (K : list ectx_item) (Î³o : gname) (N : offerReg)  :
+    k (Î³o : gname) (N : offerReg)  :
     own Î³o (â— to_offer_reg N)
-    -âˆ— own Î³o (â—¯ {[o := to_agree (v, (Î³, (j, K)))]})
-    -âˆ— âŒœN !! o = Some (v, Î³, j, K)âŒ.
+    -âˆ— own Î³o (â—¯ {[o := to_agree (v, (Î³, k))]})
+    -âˆ— âŒœN !! o = Some (v, Î³, k)âŒ.
   Proof.
     iIntros "HN Hfrag".
     iDestruct (own_valid_2 with "HN Hfrag") as %Hfoo.
@@ -110,23 +119,23 @@ Section offerReg_rules.
     intros Hav.
     rewrite -(inj Some _ _ Hav).
     rewrite Some_included_total.
-    destruct av' as [[[??]?]?]. simpl.
+    destruct av' as [[??]?]. simpl.
     rewrite to_agree_included.
     fold_leibniz.
     intros. by simplify_eq.
   Qed.
 
   Lemma offerReg_lookup_frag (o : loc) (v : val) (Î³ : gname)
-    (j : nat) (K : list ectx_item) (Î³o : gname) (N : offerReg) :
-    N !! o = Some (v, Î³, j, K) â†’
+    (k : ref_id) (Î³o : gname) (N : offerReg) :
+    N !! o = Some (v, Î³, k) â†’
     own Î³o (â— to_offer_reg N)
-    ==âˆ— own Î³o (â—¯ {[o := to_agree (v, (Î³, (j, K)))]})
+    ==âˆ— own Î³o (â—¯ {[o := to_agree (v, (Î³, k))]})
       âˆ— own Î³o (â— to_offer_reg N).
   Proof.
     iIntros (HNo) "Hown".
     iMod (own_update with "[Hown]") as "Hown".
     { eapply (auth_update (to_offer_reg N) âˆ…).
-      eapply (op_local_update_discrete _ âˆ… {[o := to_agree (v, (Î³, (j, K)))]}).
+      eapply (op_local_update_discrete _ âˆ… {[o := to_agree (v, (Î³, k))]}).
       intros. intros i. destruct (decide (i = o)); subst; rewrite lookup_op.
       + rewrite lookup_singleton lookup_fmap HNo.
         rewrite -Some_op.
@@ -142,7 +151,7 @@ Section offerReg_rules.
       rewrite right_id. iFrame "Hown". }
     iDestruct "Hown" as "[Ho Hown]".
     rewrite right_id. iFrame.
-    assert ({[o := to_agree (v, (Î³, (j, K)))]} â‹… to_offer_reg N â‰¡ to_offer_reg N) as Hfoo.
+    assert ({[o := to_agree (v, (Î³, k))]} â‹… to_offer_reg N â‰¡ to_offer_reg N) as Hfoo.
     { intro i.
       rewrite /to_offer_reg lookup_merge !lookup_fmap.
       destruct (decide (i = o)); subst.
@@ -152,7 +161,8 @@ Section offerReg_rules.
         symmetry. apply agree_included.
         by apply to_agree_included.
       + rewrite lookup_singleton_ne; eauto.
-        by rewrite left_id. }
+        destruct ((offerize <$> N !! i)) as [?|] eqn:He;
+          rewrite He; simpl; done. }
     by rewrite Hfoo.
   Qed.
 
@@ -160,9 +170,9 @@ Section offerReg_rules.
   Definition offerInv `{!relocG Î£} (N : offerReg) (f : val) : iProp Î£ :=
     ([âˆ— map] l â†¦ w âˆˆ N,
      match w with
-     | (v,Î³,j,K) => is_offer Î³ l
-                             (j â¤‡ fill K (f (of_val v))%E)
-                             (j â¤‡ fill K #())
+     | (v,Î³,k) => is_offer Î³ l
+                             (refines_right k (f (of_val v))%E)
+                             (refines_right k #())
      end)%I.
 
   Lemma offerInv_empty `{!relocG Î£} (f : val) : âŠ¢ offerInv âˆ… f.
@@ -174,7 +184,7 @@ Section offerReg_rules.
     rewrite /offerInv. iIntros "HN Ho".
     iAssert (âŒœis_Some (N !! o)âŒ â†’ False)%I as %Hbaz.
     {
-      iIntros ([[[[? ?] ?] ?] HNo]).
+      iIntros ([[[? ?] ?] HNo]).
       rewrite (big_sepM_lookup _ N o _ HNo).
       iApply (is_offer_exclusive with "HN Ho").
     }
@@ -183,6 +193,7 @@ Section offerReg_rules.
 
 End offerReg_rules.
 
+
 (** * Refinement proof *)
 Section refinement.
   Context `{!relocG Î£, !offerRegPreG Î£, !offerG Î£}.
@@ -193,40 +204,29 @@ Section refinement.
       This is also the only place where we need to unfold the definition of the refinement proposition. *)
   Lemma revoke_offer_l Î³ off E K (v : val) e1 e2 A :
     offer_token Î³ -âˆ—
-    (âˆ€ j K', (j â¤‡ fill K' e1)  ={E, âŠ¤, E}â–·=âˆ—
-      â–· is_offer Î³ off (j â¤‡ fill K' e1) (j â¤‡ fill K' e2) âˆ—
-      â–· (is_offer Î³ off (j â¤‡ fill K' e1) (j â¤‡ fill K' e2) -âˆ—
+    (âˆ€ k, refines_right k e1  ={E}[âŠ¤]â–·=âˆ—
+      â–· is_offer Î³ off (refines_right k e1) (refines_right k e2) âˆ—
+      â–· (is_offer Î³ off (refines_right k e1) (refines_right k e2) -âˆ—
            ((REL fill K (of_val NONEV) << e2 @ E : A)
          âˆ§ (REL fill K (of_val $ SOMEV v) << e1 @ E : A)))) -âˆ—
     REL fill K (revoke_offer (v, #off)%V) << e1 @ E : A.
   Proof.
     iIntros "HÎ³ Hlog".
-    rewrite {3}refines_eq /refines_def.
-    iIntros (j K') "#Hs Hj".
-    iMod ("Hlog" with "Hj") as "Hlog".
-    iModIntro. iApply wp_bind. (* TODO: why do we have to use wp_bind here? *)
+    iApply refines_split.
+    iIntros (k) "Hk".
+    iMod ("Hlog" with "Hk") as "Hlog".
+    iApply refines_wp_l.
     wp_apply (wp_revoke_offer with "HÎ³ [-]").
     iNext. iMod "Hlog" as "[Hoff Hcont]". iModIntro.
     iFrame "Hoff". iNext. iSplit.
     - iIntros "Hoff". iDestruct ("Hcont" with "Hoff") as "[Hcont _]".
-      rewrite refines_eq. by iApply "Hcont".
+      iIntros "Hk". iApply refines_left_fupd.
+      iApply (refines_combine with "Hcont Hk").
     - iIntros "Hoff". iDestruct ("Hcont" with "Hoff") as "[_ Hcont]".
-      rewrite refines_eq. by iApply "Hcont".
+      iIntros "Hk". iApply refines_left_fupd.
+      iApply (refines_combine with "Hcont Hk").
   Qed.
 
-  (** We will also use the following instances for splitting and
-  compining read-only pointsto permissions. *)
-  Local Instance ro_pointsto_fromand (l : loc) (w : val) :
-    FromSep (âˆƒ q, l â†¦{q} w) (âˆƒ q, l â†¦{q} w) (âˆƒ q, l â†¦{q} w).
-  Proof.
-    rewrite /FromSep. iIntros "[$ _]".
-  Qed.
-  Local Instance ro_pointsto_intoand (l : loc) (w : val) :
-    IntoSep (âˆƒ q, l â†¦{q} w) (âˆƒ q, l â†¦{q} w) (âˆƒ q, l â†¦{q} w).
-  Proof.
-    rewrite /IntoSep /=. iDestruct 1 as (q) "[H1 H2]".
-    iSplitL "H1"; eauto with iFrame.
-  Qed.
 
   (* ************************************************** *)
   (** ** The main invariant that we will use for the proof *)
@@ -234,17 +234,17 @@ Section refinement.
   Definition I A oname (mb : loc) (push_f : val) : iProp Î£ :=
     (âˆƒ (N : offerReg),
         (mb â†¦ NONEV      (* the mailbox is either empty or contains an offer that is in the registry *)
-        âˆ¨ (âˆƒ (l : loc) v1 v2 Î³ j K,
+        âˆ¨ (âˆƒ (l : loc) v1 v2 Î³ k,
               A v1 v2
             âˆ— mb â†¦ SOMEV (v1, #l)
-            âˆ— âŒœN !! l = Some (v2, Î³, j, K)âŒ))
+            âˆ— âŒœN !! l = Some (v2, Î³, k)âŒ))
      âˆ— own oname (â— to_offer_reg N)
      âˆ— offerInv N push_f)%I.
 
   Lemma wrap_pop_refinement A (pop1 pop2 push2 : val) Î³o mb :
     inv iN (I A Î³o mb push2) -âˆ—
-    (âˆ€ e v2 j K, j â¤‡ fill K (push2 (of_val v2)) -âˆ—
-                   (j â¤‡ fill K #() -âˆ— REL e << SOMEV v2 @ âŠ¤âˆ–â†‘iN : () + A) -âˆ—
+    (âˆ€ e v2 k, refines_right k (push2 (of_val v2)) -âˆ—
+                   (refines_right k #() -âˆ— REL e << SOMEV v2 @ âŠ¤âˆ–â†‘iN : () + A) -âˆ—
                    REL e << pop2 #() @ âŠ¤âˆ–â†‘iN : () + A) -âˆ—
     (REL pop1 << pop2 : () â†’ () + A) -âˆ—
     REL wrap_pop pop1 #mb
@@ -265,7 +265,7 @@ Section refinement.
       { iNext. iExists N; by iFrame. }
       iApply (refines_app with "Hpop"). by rel_values.
     - (* YES OFFER *)
-      iDestruct "Hmb" as (l v1 v2 Î³ j K) "(#Hv & Hmb & >HNl)".
+      iDestruct "Hmb" as (l v1 v2 Î³ k) "(#Hv & Hmb & >HNl)".
       iDestruct "HNl" as %HNl.
       rewrite /offerInv big_sepM_lookup_acc; eauto. iSimpl in "HN".
       iDestruct "HN" as "[HNl HN]".
@@ -276,7 +276,7 @@ Section refinement.
       iMod ("Hcl" with "[-Hlown IH Hpop HpopGhost]") as "_".
       { iNext. iExists _. iFrame.
         iSplitL "Hmb".
-        - iRight. iExists _, _, _, _, _, _.
+        - iRight. iExists _, _, _, _, _.
           eauto with iFrame.
         - by iApply "HN". }
 
@@ -328,20 +328,20 @@ Section refinement.
     iAssert (âˆƒ v, â–· mb â†¦ v)%I with "[Hmb]" as (v) "Hmb".
     { iDestruct "Hmb" as "[Hmb | Hmb]".
       - iExists NONEV; eauto.
-      - iDestruct "Hmb" as (l m1 m2 Î³' j K) "(Hm & Hmb & ?)".
+      - iDestruct "Hmb" as (l m1 m2 Î³' k) "(Hm & Hmb & ?)".
         iExists (SOMEV (m1, #l)); eauto. }
     iExists _; iFrame; iNext.
     iIntros "Hmb".
 
     rel_pures_l.
     rel_apply_l (revoke_offer_l with "Htok").
-    iIntros (j K') "Hj". iSpecialize ("Hoff" with "Hj").
+    iIntros (j) "Hj". iSpecialize ("Hoff" with "Hj").
     iDestruct (offerInv_excl with "HN Hoff") as %?.
-    iMod (offerReg_alloc off h2 Î³ j K' with "HNown") as "[HNown #Hfrag]"; eauto.
+    iMod (offerReg_alloc off h2 Î³ with "HNown") as "[HNown #Hfrag]"; eauto.
     iMod ("Hcl" with "[-Hpush]") as "_".
     { iNext. iExists _. iFrame "HNown".
       iSplitL "Hmb".
-      - iRight. iExists off, h1, h2, _, _, _. iFrame "Hmb Hh".
+      - iRight. iExists off, h1, h2, _, _. iFrame "Hmb Hh".
         iPureIntro. by rewrite lookup_insert.
       - rewrite /offerInv big_sepM_insert; eauto with iFrame. }
     iModIntro. iNext.
@@ -377,12 +377,12 @@ Section stack_example.
   Context `{!relocG Î£, !offerRegPreG Î£, !offerG Î£, !lockG Î£}.
 
   Definition stackI stl lk :=
-    (âˆƒ Î³, is_lock (nroot.@"LoCk") Î³ lk (âˆƒ ls1, stl â†¦{1/2} val_of_list ls1))%I.
+    (âˆƒ Î³, is_lock (nroot.@"LoCk") Î³ lk (âˆƒ ls1, stl â†¦{#1/2} val_of_list ls1))%I.
   Definition stackInv A st st' :=
     (âˆƒ (stl : loc) lk, âŒœst = (#stl, lk)%VâŒ âˆ—
        stackI stl lk âˆ—
        inv stackN (âˆƒ ls1 ls2,
-                      (stl â†¦{1/2} val_of_list ls1)
+                      (stl â†¦{#1/2} val_of_list ls1)
                     âˆ— is_stack st' ls2
                     âˆ— ([âˆ— list] v1;v2 âˆˆ ls1;ls2, A v1 v2)))%I.
 
@@ -395,23 +395,18 @@ Section stack_example.
   Proof.
     iIntros "#Hinv #Hstack".
     iApply (wrap_pop_refinement with "Hinv [] []").
-    { iIntros (e v2 j K) "Hj Hcont".
+    { iIntros (e v2 j) "Hj Hcont".
       rel_pures_r.
       iDestruct "Hstack" as (st1l lk1 ->) "[#HstI #Hstack]".
       iInv stackN as (ls1 ls2) "(Hst1 & >Hst2 & HA)" "Hcl".
       iDestruct "Hst2" as (st2l lk2 ->) "[Hlk Hst2]".
       tp_rec j. tp_pures j. tp_rec j. tp_pures j. tp_rec j.
       unlock is_locked_r. iDestruct "Hlk" as (lk' ->) "Hl".
-      (* TODO: make all the tp_ tactics work without the need for an explicit Fupd *)
-      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.
       tp_pures j. tp_rec j. tp_pures j.
       tp_load j. tp_pures j.
       tp_store j. tp_pures j.
       tp_rec j. tp_store j.
-      iClear "HÏ". iModIntro.
       rel_apply_r (refines_CG_pop_suc_r with "[Hst2 Hl]").
       { iExists st2l,#lk'. rewrite /is_locked_r. by eauto with iFrame. }
       iIntros "Hst2".
@@ -517,7 +512,7 @@ Section stack_example.
     do 5 rel_pure_r.
     rel_rec_l. rel_rec_l. rel_rec_l. rel_rec_l.
     rel_alloc_l st as "[Hst1 Hl1]". rel_pures_l.
-    rel_apply_l (refines_newlock_l (nroot.@"LoCk") (âˆƒ ls1, st â†¦{1/2} val_of_list ls1)%I with "[Hl1]").
+    rel_apply_l (refines_newlock_l (nroot.@"LoCk") (âˆƒ ls1, st â†¦{#1/2} val_of_list ls1)%I with "[Hl1]").
     { iExists []. iFrame. }
     iNext. iIntros (lk1 Î³) "#Hlk1". rel_pures_l.
     rel_alloc_l mb as "Hmb".
@@ -526,7 +521,7 @@ Section stack_example.
     iMod (own_alloc (â— to_offer_reg âˆ… : authR offerRegR)) as (Î³o) "Hor".
     { apply auth_auth_valid. apply to_offer_reg_valid. }
     iMod (inv_alloc stackN _ (âˆƒ ls1 ls2,
-                      (st â†¦{1/2} val_of_list ls1)
+                      (st â†¦{#1/2} val_of_list ls1)
                     âˆ— is_stack (#st',lk2) ls2
                     âˆ— ([âˆ— list] v1;v2 âˆˆ ls1;ls2, A v1 v2)) with "[Hst1 Hst2 Hlk2]") as "#Hinv".
     { iNext. iExists [], []; simpl; iFrame. rewrite right_id.
diff --git a/theories/experimental/helping/offers.v b/theories/experimental/helping/offers.v
index f54792c453a60061e137f8fd52b4d6e6aa7ff2fe..9ba03c8510ceb667ccfdaed81ff6705831087905 100644
--- a/theories/experimental/helping/offers.v
+++ b/theories/experimental/helping/offers.v
@@ -37,7 +37,7 @@ Section rules.
     is_offer Î³1 l P1 Q1 -âˆ— is_offer Î³2 l P2 Q2 -âˆ— False.
   Proof.
     iDestruct 1 as (?) "[Hl1 _]". iDestruct 1 as (?) "[Hl2 _]".
-    iDestruct (gen_heap.mapsto_valid_2 with "Hl1 Hl2") as %[??]. contradiction.
+    iDestruct (gen_heap.mapsto_valid_2 with "Hl1 Hl2") as %[? _]. contradiction.
   Qed.
 
   Lemma make_is_offer Î³ l P Q : l â†¦ #0 -âˆ— P -âˆ— is_offer Î³ l P Q.
diff --git a/theories/logic/adequacy.v b/theories/logic/adequacy.v
index 92c72bb7a63ad8cc171cca278d5792249c68e2ba..ccbdcea43b67d21836d72b4922ee0992abaa978b 100644
--- a/theories/logic/adequacy.v
+++ b/theories/logic/adequacy.v
@@ -16,7 +16,7 @@ Proof. solve_inG. Qed.
 
 Lemma refines_adequate Î£ `{relocPreG Î£}
   (A : âˆ€ `{relocG Î£}, lrel Î£)
-  (P : val â†’ val â†’ Prop) e e' Ïƒ :
+  (P : val â†’ val â†’ Prop) (e e' : expr) Ïƒ :
   (âˆ€ `{relocG Î£}, âˆ€ v v', A v v' -âˆ— âŒœP v v'âŒ) â†’
   (âˆ€ `{relocG Î£}, âŠ¢ REL e << e' : A) â†’
   adequate NotStuck e Ïƒ
@@ -39,11 +39,11 @@ Proof.
   iSplitL.
   - iPoseProof (Hlog _) as "Hrel".
     rewrite refines_eq /refines_def /spec_ctx.
-    iApply fupd_wp.
-    iSpecialize ("Hrel" $! 0 [] with "[Hcfg]"); first by eauto.
-    iApply "Hrel".
-    rewrite tpool_mapsto_eq /tpool_mapsto_def. iFrame.
-    by rewrite /to_tpool /= insert_empty map_fmap_singleton //.
+    iApply fupd_wp. iApply ("Hrel" $! 0 []).
+    iSplitR.
+    + iExists _. by iFrame.
+    + rewrite tpool_mapsto_eq /tpool_mapsto_def.
+      by rewrite /to_tpool /= insert_empty map_fmap_singleton //.
   - iIntros (v).
     iDestruct 1 as (v') "[Hj Hinterp]".
     rewrite HA.
@@ -59,7 +59,7 @@ Proof.
     iIntros "!> !%"; eauto.
 Qed.
 
-Theorem refines_typesafety Î£ `{relocPreG Î£} e e' e1
+Theorem refines_typesafety Î£ `{relocPreG Î£} (e e' : expr) e1
         (A : âˆ€ `{relocG Î£}, lrel Î£) thp Ïƒ Ïƒ' :
   (âˆ€ `{relocG Î£}, âŠ¢ REL e << e' : A) â†’
   rtc erased_step ([e], Ïƒ) (thp, Ïƒ') â†’ e1 âˆˆ thp â†’
diff --git a/theories/logic/compatibility.v b/theories/logic/compatibility.v
index 31f9d311590b50648e74c0245117e0fd110c91b1..7acf8e55c66d7462b2531093e76776539dcb7886 100644
--- a/theories/logic/compatibility.v
+++ b/theories/logic/compatibility.v
@@ -8,7 +8,8 @@ From reloc.logic Require Export model rules.
 From reloc.logic Require Import proofmode.tactics proofmode.spec_tactics model.
 
 Section compatibility.
-  Context `{relocG Î£}.
+  Context `{!relocG Î£}.
+  Implicit Types e : expr.
 
   Local Ltac value_case :=
     try rel_pure_l; try rel_pure_r; rel_values.
@@ -53,21 +54,6 @@ Section compatibility.
     done.
   Qed.
 
-  Lemma refines_fork e e' E :
-    â†‘relocN âŠ† E â†’
-    (REL e << e' @ E : ()) -âˆ—
-    REL Fork e << Fork e' @ E : ().
-  Proof.
-    iIntros (?) "IH".
-    rewrite refines_eq /refines_def.
-    iIntros (j K) "Hs Hj /=".
-    tp_fork j as i "Hi".
-    iMod ("IH" $! i [] with "Hs Hi") as "IH".
-    iApply (wp_fork with "[-Hj]").
-    - iNext. iApply (wp_wand with "IH"). eauto.
-    - iExists #(); eauto.
-  Qed.
-
   Lemma refines_pack (A : lrel Î£) e e' (C : lrel Î£ â†’ lrel Î£) :
     (REL e << e' : C A) -âˆ—
     REL e << e' : âˆƒ A, C A.
diff --git a/theories/logic/derived.v b/theories/logic/derived.v
index 934eef8ae252190801a5120d53a25ceacfec1959..e0ff1f8503bb570982872d3f425e27cbebd70c38 100644
--- a/theories/logic/derived.v
+++ b/theories/logic/derived.v
@@ -9,6 +9,7 @@ From reloc.logic Require Export model rules.
 Section rules.
   Context `{relocG Î£}.
   Implicit Types A : lrel Î£.
+  Implicit Types e : expr.
 
   Lemma refines_wand E e1 e2 A A' :
     (REL e1 << e2 @ E : A) -âˆ—
@@ -24,7 +25,7 @@ Section rules.
   Lemma refines_arrow (v v' : val) A A' :
     â–¡ (âˆ€ v1 v2 : val, â–¡(REL of_val v1 << of_val v2 : A) -âˆ—
       REL App v (of_val v1) << App v' (of_val v2) : A') -âˆ—
-    REL v << v' : (A â†’ A')%lrel.
+    REL (of_val v) << (of_val v') : (A â†’ A')%lrel.
   Proof.
     iIntros "#H".
     iApply refines_arrow_val; eauto.
diff --git a/theories/logic/model.v b/theories/logic/model.v
index afd17a5eef7b474ce3f03cac29f31655f580ae60..fa24ce78752a005eae6fb8f818bc3a17b258dd98 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -53,6 +53,16 @@ End lrel_ofe.
 
 Arguments lrelC : clear implicits.
 
+Record ref_id := RefId {
+  tp_id : nat;
+  tp_ctx : list ectx_item }.
+
+Canonical Structure ectx_itemO := leibnizO ectx_item.
+Canonical Structure ref_idO := leibnizO ref_id.
+
+Global Instance ref_id_inhabited : Inhabited ref_id.
+Proof. split. apply (RefId 0 []). Qed.
+
 Section semtypes.
   Context `{relocG Î£}.
 
@@ -60,10 +70,23 @@ Section semtypes.
   Implicit Types E : coPset.
   Implicit Types A B : lrel Î£.
 
+  Definition rhs_t := sum expr ref_id.
+  Definition in_1 : expr -> rhs_t := inl.
+  Definition in_2 : ref_id -> rhs_t := inr.
+  Coercion in_1 : expr >-> rhs_t.
+
+
+  Definition refines_right (k : ref_id) (e : expr) :=
+    (spec_ctx âˆ— (tp_id k) â¤‡ fill (tp_ctx k) e)%I.
+
   Definition refines_def (E : coPset)
-           (e e' : expr) (A : lrel Î£) : iProp Î£ :=
-    (âˆ€ j K, spec_ctx -âˆ— j â¤‡ fill K e'
-        ={E,âŠ¤}=âˆ— WP e {{ v, âˆƒ v', j â¤‡ fill K (of_val v') âˆ— A v v' }})%I.
+           (e : expr) (e'k : rhs_t) (A : lrel Î£) : iProp Î£ :=
+    (âˆ€ j K,
+        match e'k with
+        | inl e' => refines_right (RefId j K) e'
+        | inr k  => âŒœj = tp_id kâŒ âˆ— âŒœK = tp_ctx kâŒ
+        end -âˆ—
+        |={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.
@@ -83,7 +106,7 @@ Section semtypes.
   Definition lrel_int : lrel Î£ := LRel (Î» w1 w2, âˆƒ n : Z, âŒœ w1 = #n âˆ§ w2 = #n âŒ)%I.
 
   Definition lrel_arr (A1 A2 : lrel Î£) : lrel Î£ := LRel (Î» w1 w2,
-    â–¡ âˆ€ v1 v2, A1 v1 v2 -âˆ— refines âŠ¤ (App w1 v1) (App w2 v2) A2)%I.
+    â–¡ âˆ€ v1 v2, A1 v1 v2 -âˆ— refines âŠ¤ (App w1 v1) (in_1 (App w2 v2)) A2)%I.
 
   Definition lrel_ref (A : lrel Î£) : lrel Î£ := LRel (Î» w1 w2,
     âˆƒ l1 l2: loc, âŒœw1 = #l1âŒ âˆ§ âŒœw2 = #l2âŒ âˆ§
@@ -192,34 +215,89 @@ Section semtypes_properties.
 
 End semtypes_properties.
 
+(* Notation "'REL' e1 '<<' e2 '@' E ':' A" := *)
+(*   (refines E e1%E (inl e2%E) (A)%lrel) *)
+(*   (at level 100, E at next level, e1, e2 at next level, *)
+(*    A at level 200, *)
+(*    format "'[hv' 'REL'  e1  '/' '<<'  '/  ' e2  '@'  E  :  A ']'"). *)
+(* Notation "'REL' e1 '<<' e2 ':' A" := *)
+(*   (refines âŠ¤ e1%E (inl e2%E) (A)%lrel) *)
+(*   (at level 100, e1, e2 at next level, *)
+(*    A at level 200, *)
+(*    format "'[hv' 'REL'  e1  '/' '<<'  '/  ' e2  :  A ']'"). *)
+Notation "'REL' e1 '<<{' id '}' '_' ':' A" :=
+  (refines âŠ¤ e1%E (in_2 id) (A)%lrel)
+  (at level 100, e1 at next level,
+  A at level 200,
+  format "'[hv' 'REL'  e1  '/' '<<{' id '}' '/  '  '_'  :  A ']'").
+Notation "'REL' e1 '<<{' id '}' '_' '@' E ':' A" :=
+  (refines E e1%E (in_2 id) (A)%lrel)
+  (at level 100, E at next level, e1 at next level,
+  A at level 200,
+  format "'[hv' 'REL'  e1  '/' '<<{' id '}' '/  '  '_'  '@'  E  ':'  A ']'").
+(* (ï¿£ï½žï¿£;)  OOF *)
 Notation "'REL' e1 '<<' e2 '@' E ':' A" :=
   (refines E e1%E e2%E (A)%lrel)
   (at level 100, E at next level, e1, e2 at next level,
    A at level 200,
    format "'[hv' 'REL'  e1  '/' '<<'  '/  ' e2  '@'  E  :  A ']'").
-Notation "'REL' e1 '<<' e2 ':' A" :=
-  (refines âŠ¤ e1%E e2%E (A)%lrel)
-  (at level 100, e1, e2 at next level,
+Notation "'REL' e1 '<<' t ':' A" :=
+  (refines âŠ¤ e1%E t%E (A)%lrel)
+  (at level 100, e1, t at next level,
    A at level 200,
-   format "'[hv' 'REL'  e1  '/' '<<'  '/  ' e2  :  A ']'").
+   format "'[hv' 'REL'  e1  '/' '<<'  '/  ' t  :  A ']'").
 
 (** Properties of the relational interpretation *)
 Section related_facts.
-  Context `{relocG Î£}.
+  Context `{!relocG Î£}.
+  Implicit Types e : expr.
+
+
+  Lemma refines_split E e e' A :
+    (âˆ€ k, refines_right k e' -âˆ— REL e <<{k} _ @ E : A) -âˆ—
+    REL e << e' @ E : A.
+  Proof.
+    iIntros "H".
+    rewrite refines_eq /refines_def.
+    iIntros (j K) "He'". pose (k := RefId j K).
+    iSpecialize ("H" $! k with "He'").
+    by iApply "H".
+  Qed.
+
+  Lemma refines_combine E e e' A k :
+    (REL e << e' @ E : A) -âˆ—
+    refines_right k e' -âˆ—
+    REL e <<{k} _ @ E : A.
+  Proof.
+    iIntros "H1 H2".
+    rewrite refines_eq /refines_def.
+    iIntros (j K) "[% %]".
+    iApply "H1". by destruct k; simplify_eq/=.
+  Qed.
 
   (* We need this to be able to open and closed invariants in front of logrels *)
-  Lemma fupd_refines E1 E2 e e' A :
-    (|={E1,E2}=> REL e << e' @ E2 : A) -âˆ— REL e << e' @ E1 : A.
+  Lemma fupd_refines E1 E2 e t A :
+    (|={E1, E2}=> refines E2 e t A) -âˆ— refines E1 e t A.
+  Proof.
+    rewrite refines_eq /refines_def.
+    iIntros "H". iIntros (j K) "Hr /=".
+    iMod "H" as "H". iApply ("H" with "Hr").
+  Qed.
+
+  Lemma refines_left_fupd E e k A :
+    (REL e <<{k} _ @ E : A) ={E,âŠ¤}=âˆ— REL e <<{k} _ @ âŠ¤ : A.
   Proof.
     rewrite refines_eq /refines_def.
-    iIntros "H". iIntros (j K) "#Hs Hj /=".
-    iMod "H" as "H". iApply ("H" with "Hs Hj").
+    iIntros "H". simpl.
+    iSpecialize ("H" $! (tp_id k) (tp_ctx k) with "[%//]").
+    iMod "H" as "H". iModIntro.
+    iIntros (j K) "[-> ->]". done.
   Qed.
 
-  Global Instance elim_fupd_refines p E1 E2 e e' P A :
+  Global Instance elim_fupd_refines p E1 E2 e t P A :
    (* TODO: DF: look at the booleans here *)
    ElimModal True p false (|={E1,E2}=> P) P
-     (REL e << e' @ E1 : A) (REL e << e' @ E2: A).
+     (refines E1 e t A) (refines E2 e t A).
   Proof.
     rewrite /ElimModal. intros _.
     iIntros "[HP HI]". iApply fupd_refines.
@@ -227,51 +305,43 @@ Section related_facts.
     iMod "HP"; iModIntro; by iApply "HI".
   Qed.
 
-  Global Instance elim_bupd_logrel p E e e' P A :
+  Global Instance elim_bupd_logrel p E e t P A :
    ElimModal True p false (|==> P) P
-     (REL e << e' @ E : A) (REL e << e' @ E : A).
+     (refines E e t A) (refines E e t A).
   Proof.
     rewrite /ElimModal (bupd_fupd E).
     apply: elim_fupd_refines.
   Qed.
 
   (* This + elim_modal_timless_bupd' is useful for stripping off laters of timeless propositions. *)
-  Global Instance is_except_0_logrel E e e' A :
-    IsExcept0 (REL e << e' @ E : A).
+  Global Instance is_except_0_logrel E e t A :
+    IsExcept0 (refines E e t A).
   Proof.
     rewrite /IsExcept0. iIntros "HL".
     iApply fupd_refines. 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 (j K) "#Hspec".
-    by iApply "Hctx".
-  Qed.
 End related_facts.
 
 Section monadic.
-  Context `{relocG Î£}.
+  Context `{!relocG Î£}.
+  Implicit Types e : expr.
 
   Lemma refines_bind K K' E A A' e e' :
     (REL e << e' @ E : A) -âˆ—
     (âˆ€ v v', A v v' -âˆ—
-      REL fill K (of_val v) << fill K' (of_val v') : A') -âˆ—
+      REL fill K (of_val v) << (fill K' (of_val v')) : A') -âˆ—
     REL fill K e << fill K' e' @ E : A'.
   Proof.
     iIntros "Hm Hf".
-    rewrite refines_eq /refines_def.
-    iIntros (j Kâ‚) "#Hs Hj /=".
-    iSpecialize ("Hm" with "Hs").
-    rewrite -fill_app. iMod ("Hm" with "Hj") as "Hm".
+    rewrite refines_eq /refines_def /refines_right.
+    iIntros (j Kâ‚) "[#Hs Hj] /=".
+    rewrite -fill_app.
+    iMod ("Hm" with "[$Hs $Hj]") as "Hm".
     iModIntro. iApply wp_bind.
     iApply (wp_wand with "Hm").
     iIntros (v). iDestruct 1 as (v') "[Hj HA]".
     rewrite fill_app.
-    by iMod ("Hf" with "HA Hs Hj") as "Hf/=".
+    by iMod ("Hf" with "HA [$Hs $Hj]") as "Hf/=".
   Qed.
 
   Lemma refines_ret E e1 e2 v1 v2 (A : lrel Î£) :
@@ -279,9 +349,10 @@ Section monadic.
     IntoVal e2 v2 â†’
     (|={E,âŠ¤}=> A v1 v2) -âˆ— REL e1 << e2 @ E : A.
   Proof.
+    rewrite /IntoVal.
     iIntros (<-<-) "HA".
     rewrite refines_eq /refines_def.
-    iIntros (j K) "#Hs 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 4635215d88256c8b18cfcfcaa6363fdf7ea9d434..355979984ca35d48bfc8e6e30f1d128ba44cd025 100644
--- a/theories/logic/proofmode/spec_tactics.v
+++ b/theories/logic/proofmode/spec_tactics.v
@@ -10,10 +10,10 @@ Set Default Proof Using "Type".
 (** * TP tactics *)
 
 (** ** bind *)
-Lemma tac_tp_bind_gen `{relocG Î£} j Î” Î”' i p e e' Q :
-  envs_lookup i Î” = Some (p, j â¤‡ e)%I â†’
+Lemma tac_tp_bind_gen `{relocG Î£} k Î” Î”' i p e e' Q :
+  envs_lookup i Î” = Some (p, refines_right k e)%I â†’
   e = e' â†’
-  envs_simple_replace i p (Esnoc Enil i (j â¤‡ e')) Î” = Some Î”' â†’
+  envs_simple_replace i p (Esnoc Enil i (refines_right k e')) Î” = Some Î”' â†’
   (envs_entails Î”' Q) â†’
   (envs_entails Î” Q).
 Proof.
@@ -22,10 +22,10 @@ Proof.
   destruct p; rewrite /= ?right_id; by rewrite bi.wand_elim_r.
 Qed.
 
-Lemma tac_tp_bind `{relocG Î£} j e' Î” Î”' i p K' e Q :
-  envs_lookup i Î” = Some (p, j â¤‡ e)%I â†’
+Lemma tac_tp_bind `{relocG Î£} k e' Î” Î”' i p K' e Q :
+  envs_lookup i Î” = Some (p, refines_right k e)%I â†’
   e = fill K' e' â†’
-  envs_simple_replace i p (Esnoc Enil i (j â¤‡ fill K' e')) Î” = Some Î”' â†’
+  envs_simple_replace i p (Esnoc Enil i (refines_right k (fill K' e'))) Î” = Some Î”' â†’
   (envs_entails Î”' Q) â†’
   (envs_entails Î” Q).
 Proof. intros. by eapply tac_tp_bind_gen. Qed.
@@ -64,7 +64,7 @@ Tactic Notation "tp_bind" constr(j) open_constr(efoc) :=
     |reflexivity
     |(* new goal *)].
 
-Lemma tac_tp_pure `{relocG Î£} e K' e1 j e2 Î”1 E1 i1 i2 p e' Ï• Ïˆ Q n :
+Lemma tac_tp_pure `{relocG Î£} e K' e1 k e2 Î”1 E1 i1 e' Ï• Ïˆ Q n :
   (* we have those premises first, because we will be trying to solve them
      with backtracking using reashape_expr; see the accompanying Ltac.
      the first premise decomposes the expression, the second one checks
@@ -73,32 +73,23 @@ Lemma tac_tp_pure `{relocG Î£} e K' e1 j e2 Î”1 E1 i1 i2 p e' Ï• Ïˆ Q n :
   PureExec Ï• n e1 e2 â†’
   (âˆ€ P, ElimModal Ïˆ false false (|={E1}=> P) P Q Q) â†’
   nclose specN âŠ† E1 â†’
-  envs_lookup i1 Î”1 = Some (p, spec_ctx) â†’
-  envs_lookup i2 Î”1 = Some (false, j â¤‡ e)%I â†’
+  envs_lookup i1 Î”1 = Some (false, refines_right k e)%I â†’
   Ïˆ â†’
   Ï• â†’
   (* we will call simpl on this goal thus re-composing the expression again *)
   e' = fill K' e2 â†’
-  match envs_simple_replace i2 false (Esnoc Enil i2 (j â¤‡ e')) Î”1 with
+  match envs_simple_replace i1 false (Esnoc Enil i1 (refines_right k e')) Î”1 with
   | Some Î”2 => envs_entails Î”2 Q
   | None => False
   end â†’
   envs_entails Î”1 Q.
 Proof.
-  rewrite envs_entails_eq. intros -> Hpure ?? HÎ”1 ? HÏˆ HÏ• -> ?.
-  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 <-.
-  { rewrite -bi.intuitionistically_into_persistently_1.
-    destruct p; simpl;
-    by rewrite ?(bi.intuitionistic_intuitionistically spec_ctx). }
-  rewrite bi.persistently_and_intuitionistically_sep_l.
-  rewrite bi.intuitionistic_intuitionistically.
+  rewrite envs_entails_eq. intros -> Hpure ?? HÎ”1 HÏˆ HÏ• -> ?.
   destruct (envs_simple_replace _ _ _ _) as [Î”2|] eqn:HÎ”2; try done.
-  rewrite (envs_simple_replace_sound Î”1 Î”2 i2) //; simpl.
+  rewrite (envs_simple_replace_sound Î”1 Î”2 i1) //; simpl.
   rewrite right_id.
-  rewrite (assoc _ spec_ctx (j â¤‡ _)%I).
+  rewrite /refines_right.
+  rewrite -!fill_app.
   rewrite step_pure //.
   rewrite -[Q]elim_modal // /=.
   apply bi.sep_mono_r.
@@ -106,40 +97,28 @@ Proof.
   by rewrite bi.wand_elim_r.
 Qed.
 
-(* helper tactic allowing us to use tp_ tactics whenever our goal is a refinement *)
-Ltac with_spec_ctx tac :=
-  lazymatch goal with
-  | |- envs_entails _ (refines ?E ?e1 ?e2 ?A) =>
-    let H := iFresh in
-    iApply (refines_spec_ctx E e1 e2 A);
-    iIntros H;
-    (tac (); iClear H)
-  | _ => tac ()
-  end.
-
 Tactic Notation "tp_pure" constr(j) open_constr(ef) :=
   iStartProof;
-  with_spec_ctx ltac:(fun _ =>
-      lazymatch goal with
-      | |- context[environments.Esnoc _ ?H (j â¤‡ fill ?K' ?e)] =>
-        reshape_expr e ltac:(fun K e' =>
-            unify e' ef;
-            eapply (tac_tp_pure (fill K' e) (K++K') e' j);
-            [by rewrite ?fill_app | iSolveTC | ..])
-      | |- context[environments.Esnoc _ ?H (j â¤‡ ?e)] =>
-        reshape_expr e ltac:(fun K e' =>
-            unify e' ef;
-            eapply (tac_tp_pure e K e' j);
-            [by rewrite ?fill_app | iSolveTC | ..])
-      end;
-      [iSolveTC || fail "tp_pure: cannot eliminate modality in the goal"
-      |solve_ndisj || fail "tp_pure: cannot prove 'nclose specN âŠ† ?'"
-      |iAssumptionCore || fail "tp_pure: cannot find spec_ctx" (* spec_ctx *)
-      |iAssumptionCore || fail "tp_pure: cannot find '" j " â¤‡ ?'"
-      |try (exact I || reflexivity) (* Ïˆ *)
-      |try (exact I || reflexivity) (* Ï• *)
-      |simpl; reflexivity ||  fail "tp_pure: this should not happen" (* e' = fill K' e2 *)
-      |pm_reduce (* new goal *)]).
+  lazymatch goal with
+  | |- context[environments.Esnoc _ ?H (refines_right j (fill ?K' ?e))] =>
+    reshape_expr e ltac:(fun K e' =>
+      unify e' ef;
+      eapply (tac_tp_pure (fill K' e) (K++K') e' j);
+      [by rewrite ?fill_app | iSolveTC | ..])
+  | |- context[environments.Esnoc _ ?H (refines_right j ?e)] =>
+    reshape_expr e ltac:(fun K e' =>
+      unify e' ef;
+      eapply (tac_tp_pure e K e' j);
+      [by rewrite ?fill_app | iSolveTC | ..])
+  end;
+  [iSolveTC || fail "tp_pure: cannot eliminate modality in the goal"
+  |solve_ndisj || fail "tp_pure: cannot prove 'nclose specN âŠ† ?'"
+  (* |iAssumptionCore || fail "tp_pure: cannot find spec_ctx" (* spec_ctx *) *)
+  |iAssumptionCore || fail "tp_pure: cannot find the RHS" (* TODO fix error message *)
+  |try (exact I || reflexivity) (* Ïˆ *)
+  |try (exact I || reflexivity) (* Ï• *)
+  |simpl; reflexivity ||  fail "tp_pure: this should not happen" (* e' = fill K' e2 *)
+  |pm_reduce (* new goal *)].
 
 
 Tactic Notation "tp_pures" constr (j) := repeat (tp_pure j _).
@@ -165,174 +144,145 @@ 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 E1 i1 i2 i3 p K' e (l : loc) e' e2 v' v Q :
+Lemma tac_tp_store `{relocG Î£} k Î”1 Î”2 E1 i1 i2 K' e (l : loc) e' e2 v' v Q :
   (* TODO: here instead of True we can consider another Coq premise, like in tp_pure.
      Same goes for the rest of those tactics *)
   (âˆ€ P, ElimModal True false false (|={E1}=> P) P Q Q) â†’
   nclose specN âŠ† E1 â†’
-  envs_lookup i1 Î”1 = Some (p, spec_ctx) â†’
-  envs_lookup_delete false i2 Î”1 = Some (false, j â¤‡ e, Î”2)%I â†’
+  envs_lookup_delete false i1 Î”1 = Some (false, refines_right k e, Î”2)%I â†’
   e = fill K' (Store (# l) e') â†’
   IntoVal e' v â†’
   (* re-compose the expression and the evaluation context *)
   e2 = fill K' #() â†’
-  envs_lookup i3 Î”2 = Some (false, l â†¦â‚› v')%I â†’
-  match envs_simple_replace i3 false
-     (Esnoc (Esnoc Enil i2 (j â¤‡ e2)) i3 (l â†¦â‚› v)) Î”2 with
+  envs_lookup i2 Î”2 = Some (false, l â†¦â‚› v')%I â†’
+  match envs_simple_replace i2 false
+     (Esnoc (Esnoc Enil i1 (refines_right k e2)) i2 (l â†¦â‚› v)) Î”2 with
   | None => False
   | Some Î”3 => envs_entails Î”3 Q
   end â†’
   envs_entails Î”1 Q.
 Proof.
-  rewrite envs_entails_eq. intros ???? -> <- -> ? HQ.
-  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.
-  { rewrite -Hq.
-    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). }
+  rewrite /IntoVal.
+  rewrite envs_entails_eq. intros ??? -> <- -> ? HQ.
   rewrite envs_lookup_delete_sound //; simpl.
   destruct (envs_simple_replace _ _ _ _) as [Î”3|] eqn:HÎ”3; last done.
   rewrite envs_simple_replace_sound //; simpl.
   rewrite right_id.
   rewrite !assoc -(assoc _ spec_ctx).
-  rewrite step_store //.
+  rewrite -fill_app step_store // fill_app.
   rewrite -[Q]elim_modal //.
   apply bi.sep_mono_r.
   apply bi.wand_intro_l.
-  rewrite (comm _ _ (l â†¦â‚› v)%I).
+  rewrite (comm _ _ (l â†¦â‚› v)%I). simpl.
+  rewrite assoc. rewrite (comm _ spec_ctx (l â†¦â‚› _)%I).
   by rewrite bi.wand_elim_r.
 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 âŠ† ?'"
-        |iAssumptionCore || fail "tp_store: cannot find spec_ctx" (* spec_ctx *)
-        |iAssumptionCore || fail "tp_store: cannot find '" j " â¤‡ ?'"
-        |tp_bind_helper
-        |iSolveTC || fail "tp_store: cannot convert the argument to a value"
-        |simpl; reflexivity || fail "tp_store: this should not happen"
-        |iAssumptionCore || fail "tp_store: cannot find '? â†¦â‚› ?'"
-        |pm_reduce (* new goal *)]).
-
-(*
-DF:
-If [envs_lookup i1 Î”1 = Some (p, spec_ctx Ï)] and
-   [envs_lookup i2 Î”1 = Some (false, j â¤‡ fill K e)],
-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 E1 i1 i2 i3 p K' e e2 (l : loc) v Q q :
+  eapply (tac_tp_store j);
+  [iSolveTC || fail "tp_store: cannot eliminate modality in the goal"
+  |solve_ndisj || fail "tp_store: cannot prove 'nclose specN âŠ† ?'"
+  |iAssumptionCore || fail "tp_store: cannot find '" j " ' RHS"
+  |tp_bind_helper
+  |iSolveTC || fail "tp_store: cannot convert the argument to a value"
+  |simpl; reflexivity || fail "tp_store: this should not happen"
+  |iAssumptionCore || fail "tp_store: cannot find '? â†¦â‚› ?'"
+  |pm_reduce (* new goal *)].
+
+(* *)
+(* DF: *)
+(* If [envs_lookup i1 Î”1 = Some (p, spec_ctx Ï)] and *)
+(*    [envs_lookup i2 Î”1 = Some (false, j â¤‡ fill K e)], *)
+(* 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 Î£} k Î”1 Î”2 E1 i1 i2 K' e e2 (l : loc) v Q q :
   (âˆ€ P, ElimModal True false false (|={E1}=> P) P Q Q) â†’
   nclose specN âŠ† E1 â†’
-  envs_lookup i1 Î”1 = Some (p, spec_ctx) â†’
-  envs_lookup_delete false i2 Î”1 = Some (false, j â¤‡ e, Î”2)%I â†’
+  envs_lookup_delete false i1 Î”1 = Some (false, refines_right k e, Î”2)%I â†’
   e = fill K' (Load #l) â†’
-  envs_lookup i3 Î”2 = Some (false, l â†¦â‚›{q} v)%I â†’
+  envs_lookup i2 Î”2 = Some (false, l â†¦â‚›{q} v)%I â†’
   e2 = fill K' (of_val v) â†’
-  match envs_simple_replace i3 false
-    (Esnoc (Esnoc Enil i2 (j â¤‡ e2)) i3 (l â†¦â‚›{q} v)%I) Î”2 with
+  match envs_simple_replace i2 false
+    (Esnoc (Esnoc Enil i1 (refines_right k e2)) i2 (l â†¦â‚›{q} v)%I) Î”2 with
   | Some Î”3 => envs_entails Î”3 Q
   | None    => False
   end â†’
   envs_entails Î”1 Q.
 Proof.
-  rewrite envs_entails_eq. intros ???? -> ? -> HQ.
-  rewrite -(idemp bi_and (of_envs Î”1)).
-  rewrite {1}(envs_lookup_sound' Î”1 false); last by eassumption.
-  rewrite bi.sep_elim_l.
-  enough (spec_ctx âˆ— of_envs Î”1 -âˆ— Q) as Hq.
-  { rewrite -Hq.
-    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). }
+  rewrite envs_entails_eq. intros ??? -> ? -> HQ.
   rewrite envs_lookup_delete_sound //; simpl.
   destruct (envs_simple_replace _ _ _ _) as [Î”3|] eqn:HÎ”3; last done.
-  rewrite (envs_simple_replace_sound Î”2 Î”3 i3) //; simpl.
+  rewrite (envs_simple_replace_sound Î”2 Î”3 i2) //; simpl.
+  rewrite /refines_right.
   rewrite right_id.
-  rewrite (assoc _ spec_ctx (j â¤‡ fill K' (Load _))%I).
-  rewrite assoc.
-  rewrite -(assoc _ spec_ctx (j â¤‡ fill K' (Load _))%I).
-  rewrite step_load //.
+  rewrite assoc. rewrite -(assoc _ spec_ctx).
+  rewrite -fill_app step_load /= // fill_app.
   rewrite -[Q]elim_modal //.
   apply bi.sep_mono_r.
   apply bi.wand_intro_l.
   rewrite (comm _ _ (l â†¦â‚›{q} v)%I).
+  rewrite assoc.
+  rewrite (comm _ _ (l â†¦â‚›{q} v)%I).
+  rewrite -assoc.
   rewrite HQ. by apply bi.wand_elim_r.
 Qed.
 
 Tactic Notation "tp_load" constr(j) :=
   iStartProof;
-  with_spec_ctx ltac:(fun _ =>
-      eapply (tac_tp_load j);
-        [iSolveTC || fail "tp_load: cannot eliminate modality in the goal"
-        |solve_ndisj || fail "tp_load: cannot prove 'nclose specN âŠ† ?'"
-        |iAssumptionCore || fail "tp_load: cannot find spec_ctx" (* spec_ctx *)
-        |iAssumptionCore || fail "tp_load: cannot find '" j " â¤‡ ?'"
-        |tp_bind_helper
-        |iAssumptionCore || fail "tp_load: cannot find '? â†¦â‚› ?'"
-        |simpl; reflexivity || fail "tp_load: this should not happen"
-        |pm_reduce (* new goal *)]).
-
-Lemma tac_tp_cmpxchg_fail `{relocG Î£} j Î”1 Î”2 E1 i1 i2 i3 p K' e enew (l : loc) e1 e2 v' v1 v2 Q q :
+  eapply (tac_tp_load j);
+  [iSolveTC || fail "tp_load: cannot eliminate modality in the goal"
+  |solve_ndisj || fail "tp_load: cannot prove 'nclose specN âŠ† ?'"
+  |iAssumptionCore || fail "tp_load: cannot find the RHS '" j "'"
+  |tp_bind_helper
+  |iAssumptionCore || fail "tp_load: cannot find '? â†¦â‚› ?'"
+  |simpl; reflexivity || fail "tp_load: this should not happen"
+  |pm_reduce (* new goal *)].
+
+Lemma tac_tp_cmpxchg_fail `{relocG Î£} k Î”1 Î”2 E1 i1 i2 K' e enew (l : loc) e1 e2 v' v1 v2 Q q :
   (âˆ€ P, ElimModal True false false (|={E1}=> P) P Q Q) â†’
   nclose specN âŠ† E1 â†’
-  envs_lookup i1 Î”1 = Some (p, spec_ctx) â†’
-  envs_lookup_delete false i2 Î”1 = Some (false, j â¤‡ e, Î”2)%I â†’
+  envs_lookup_delete false i1 Î”1 = Some (false, refines_right k e, Î”2)%I â†’
   e = fill K' (CmpXchg #l e1 e2) â†’
   IntoVal e1 v1 â†’
   IntoVal e2 v2 â†’
-  envs_lookup i3 Î”2 = Some (false, l â†¦â‚›{q} v')%I â†’
+  envs_lookup i2 Î”2 = Some (false, l â†¦â‚›{q} v')%I â†’
   v' â‰  v1 â†’
   vals_compare_safe v' v1 â†’
   enew = fill K' (v', #false)%V â†’
-  match envs_simple_replace i3 false
-    (Esnoc (Esnoc Enil i2 (j â¤‡ enew)) i3 (l â†¦â‚›{q} v')%I) Î”2 with
+  match envs_simple_replace i2 false
+    (Esnoc (Esnoc Enil i1 (refines_right k enew)) i2 (l â†¦â‚›{q} v')%I) Î”2 with
   | Some Î”3 => envs_entails Î”3 Q
   | None    =>  False
   end â†’
   envs_entails Î”1 Q.
 Proof.
-  rewrite envs_entails_eq. intros ???? -> Hv1 Hv2 ??? -> HQ.
-  rewrite -(idemp bi_and (of_envs Î”1)).
-  rewrite {1}(envs_lookup_sound' Î”1 false); last by eassumption.
-  rewrite bi.sep_elim_l.
-  enough (spec_ctx âˆ— of_envs Î”1 -âˆ— Q) as Hq.
-  { rewrite -Hq.
-    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). }
+  rewrite envs_entails_eq. intros ??? -> Hv1 Hv2 ??? -> HQ.
   rewrite envs_lookup_delete_sound //; simpl.
   destruct (envs_simple_replace _ _ _ _) as [Î”3|] eqn:HÎ”3; last done.
-  rewrite (envs_simple_replace_sound Î”2 Î”3 i3) //; simpl.
+  rewrite (envs_simple_replace_sound Î”2 Î”3 i2) //; simpl.
   rewrite right_id.
-  (* (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 step_cmpxchg_fail //.
+  rewrite /refines_right. rewrite -fill_app.
+  rewrite assoc. rewrite -(assoc _ spec_ctx).
+  rewrite step_cmpxchg_fail //. rewrite fill_app.
   rewrite -[Q]elim_modal //.
   apply bi.sep_mono_r.
   apply bi.wand_intro_l.
   rewrite (comm _ _ (l â†¦â‚›{q} _)%I).
+  rewrite assoc.
+  rewrite (comm _ _ (l â†¦â‚›{q} _)%I).
+  rewrite -assoc.
   rewrite HQ. by apply bi.wand_elim_r.
 Qed.
 
 Tactic Notation "tp_cmpxchg_fail" constr(j) :=
   iStartProof;
-  with_spec_ctx ltac:(fun _ =>
   eapply (tac_tp_cmpxchg_fail j);
     [iSolveTC || fail "tp_cmpxchg_fail: cannot eliminate modality in the goal"
     |solve_ndisj || fail "tp_cmpxchg_fail: cannot prove 'nclose specN âŠ† ?'"
-    |iAssumptionCore || fail "tp_cmpxchg_fail: cannot find spec_ctx" (* spec_ctx *)
-    |iAssumptionCore || fail "tp_cmpxchg_fail: cannot find '" j " â¤‡ ?'"
+    |iAssumptionCore || fail "tp_cmpxchg_fail: cannot find the RHS '" j "'"
     |tp_bind_helper (* e = K'[CmpXchg _ _ _] *)
     |iSolveTC || fail "tp_cmpxchg_fail: argument is not a value"
     |iSolveTC || fail "tp_cmpxchg_fail: argument is not a value"
@@ -340,234 +290,191 @@ Tactic Notation "tp_cmpxchg_fail" constr(j) :=
     |try (simpl; congruence) (* v' â‰  v1 *)
     |try heap_lang.proofmode.solve_vals_compare_safe
     |simpl; reflexivity || fail "tp_cmpxchg_fail: this should not happen"
-    |pm_reduce (* new goal *)]).
+    |pm_reduce (* new goal *)].
 
-Lemma tac_tp_cmpxchg_suc `{relocG Î£} j Î”1 Î”2 E1 i1 i2 i3 p K' e enew (l : loc) e1 e2 v' v1 v2 Q :
+Lemma tac_tp_cmpxchg_suc `{relocG Î£} k Î”1 Î”2 E1 i1 i2 K' e enew (l : loc) e1 e2 v' v1 v2 Q :
   (âˆ€ P, ElimModal True false false (|={E1}=> P) P Q Q) â†’
   nclose specN âŠ† E1 â†’
-  envs_lookup i1 Î”1 = Some (p, spec_ctx) â†’
-  envs_lookup_delete false i2 Î”1 = Some (false, j â¤‡ e, Î”2)%I â†’
+  envs_lookup_delete false i1 Î”1 = Some (false, refines_right k e, Î”2)%I â†’
   e = fill K' (CmpXchg #l e1 e2) â†’
   IntoVal e1 v1 â†’
   IntoVal e2 v2 â†’
-  envs_lookup i3 Î”2 = Some (false, l â†¦â‚› v')%I â†’
+  envs_lookup i2 Î”2 = Some (false, l â†¦â‚› v')%I â†’
   v' = v1 â†’
   vals_compare_safe v' v1 â†’
   enew = fill K' (v', #true)%V â†’
-  match envs_simple_replace i3 false
-    (Esnoc (Esnoc Enil i2 (j â¤‡ enew)) i3 (l â†¦â‚› v2)%I) Î”2 with
+  match envs_simple_replace i2 false
+    (Esnoc (Esnoc Enil i1 (refines_right k enew)) i2 (l â†¦â‚› v2)%I) Î”2 with
   | Some Î”3 => envs_entails Î”3 Q
   | None => False
   end â†’
   envs_entails Î”1 Q.
 Proof.
-  rewrite envs_entails_eq. intros ???? -> Hv1 Hv2 ??? -> HQ.
-  rewrite -(idemp bi_and (of_envs Î”1)).
-  rewrite {1}(envs_lookup_sound' Î”1 false); last by eassumption.
-  rewrite bi.sep_elim_l.
-  enough (spec_ctx âˆ— of_envs Î”1 -âˆ— Q) as Hq.
-  { rewrite -Hq.
-    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). }
+  rewrite envs_entails_eq. intros ??? -> Hv1 Hv2 ??? -> HQ.
   rewrite envs_lookup_delete_sound //; simpl.
   destruct (envs_simple_replace _ _ _ _) as [Î”3|] eqn:HÎ”3; last done.
-  rewrite (envs_simple_replace_sound Î”2 Î”3 i3) //; simpl.
+  rewrite (envs_simple_replace_sound Î”2 Î”3 i2) //; simpl.
   rewrite right_id.
-  (* (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 step_cmpxchg_suc //.
+  rewrite /refines_right. rewrite -fill_app.
+  rewrite assoc. rewrite -(assoc _ spec_ctx).
+  rewrite step_cmpxchg_suc //. rewrite fill_app.
   rewrite -[Q]elim_modal //.
   apply bi.sep_mono_r.
   apply bi.wand_intro_l.
-  rewrite (comm _ _ (l â†¦â‚› _)%I).
+  rewrite (comm _ _ (l â†¦â‚› _)%I) assoc.
+  rewrite (comm _ _ (l â†¦â‚› _)%I) -assoc.
   rewrite HQ. by apply bi.wand_elim_r.
 Qed.
 
 Tactic Notation "tp_cmpxchg_suc" constr(j) :=
   iStartProof;
-  with_spec_ctx ltac:(fun _ =>
-      eapply (tac_tp_cmpxchg_suc j);
-        [iSolveTC || fail "tp_cmpxchg_suc: cannot eliminate modality in the goal"
-        |solve_ndisj || fail "tp_cmpxchg_suc: cannot prove 'nclose specN âŠ† ?'"
-        |iAssumptionCore || fail "tp_cmpxchg_suc: cannot find spec_ctx" (* spec_ctx *)
-        |iAssumptionCore || fail "tp_cmpxchg_suc: cannot find '" j " â¤‡ ?'"
-        |tp_bind_helper (* e = K'[CmpXchg _ _ _] *)
-        |iSolveTC || fail "tp_cmpxchg_suc: argument is not a value"
-        |iSolveTC || fail "tp_cmpxchg_suc: argument is not a value"
-        |iAssumptionCore || fail "tp_cmpxchg_suc: cannot find '? â†¦ ?'"
-        |try (simpl; congruence)     (* v' = v1 *)
-        |try heap_lang.proofmode.solve_vals_compare_safe
-        |simpl; reflexivity || fail "tp_cmpxchg_suc: this should not happen"
-        |pm_reduce (* new goal *)]).
-
-Lemma tac_tp_faa `{relocG Î£} j Î”1 Î”2 E1 i1 i2 i3 p K' e enew (l : loc)  e2 (z1 z2 : Z) Q :
+  eapply (tac_tp_cmpxchg_suc j);
+  [iSolveTC || fail "tp_cmpxchg_suc: cannot eliminate modality in the goal"
+  |solve_ndisj || fail "tp_cmpxchg_suc: cannot prove 'nclose specN âŠ† ?'"
+  |iAssumptionCore || fail "tp_cmpxchg_suc: cannot the RHS '" j "'"
+  |tp_bind_helper (* e = K'[CmpXchg _ _ _] *)
+  |iSolveTC || fail "tp_cmpxchg_suc: argument is not a value"
+  |iSolveTC || fail "tp_cmpxchg_suc: argument is not a value"
+  |iAssumptionCore || fail "tp_cmpxchg_suc: cannot find '? â†¦ ?'"
+  |try (simpl; congruence)     (* v' = v1 *)
+  |try heap_lang.proofmode.solve_vals_compare_safe
+  |simpl; reflexivity || fail "tp_cmpxchg_suc: this should not happen"
+  |pm_reduce (* new goal *)].
+
+Lemma tac_tp_faa `{relocG Î£} k Î”1 Î”2 E1 i1 i2 K' e enew (l : loc)  e2 (z1 z2 : Z) Q :
   (âˆ€ P, ElimModal True false false (|={E1}=> P) P Q Q) â†’
   nclose specN âŠ† E1 â†’
-  envs_lookup i1 Î”1 = Some (p, spec_ctx) â†’
-  envs_lookup_delete false i2 Î”1 = Some (false, j â¤‡ e, Î”2)%I â†’
+  envs_lookup_delete false i1 Î”1 = Some (false, refines_right k e, Î”2)%I â†’
   e = fill K' (FAA #l e2) â†’
   IntoVal e2 #z2 â†’
-  envs_lookup i3 Î”2 = Some (false, l â†¦â‚› #z1)%I â†’
+  envs_lookup i2 Î”2 = Some (false, l â†¦â‚› #z1)%I â†’
   enew = fill K' #z1 â†’
-  match envs_simple_replace i3 false
-    (Esnoc (Esnoc Enil i2 (j â¤‡ enew)) i3 (l â†¦â‚› #(z1+z2))%I) Î”2 with
+  match envs_simple_replace i2 false
+    (Esnoc (Esnoc Enil i1 (refines_right k enew)) i2 (l â†¦â‚› #(z1+z2))%I) Î”2 with
     | Some Î”3 =>   envs_entails Î”3 Q
     | None => False
   end â†’
   envs_entails Î”1 Q.
 Proof.
-  rewrite envs_entails_eq. intros ???? -> ?? -> HQ.
-  rewrite -(idemp bi_and (of_envs Î”1)).
-  rewrite {1}(envs_lookup_sound' Î”1 false); last by eassumption.
-  rewrite bi.sep_elim_l.
-  enough (spec_ctx âˆ— of_envs Î”1 -âˆ— Q) as Hq.
-  { rewrite -Hq.
-    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). }
+  rewrite envs_entails_eq. intros ??? -> ?? -> HQ.
   rewrite envs_lookup_delete_sound //; simpl.
   destruct (envs_simple_replace _ _ _ _) as [Î”3|] eqn:HÎ”3; last done.
-  rewrite (envs_simple_replace_sound Î”2 Î”3 i3) //; simpl.
+  rewrite (envs_simple_replace_sound Î”2 Î”3 i2) //; simpl.
   rewrite right_id.
-  (* (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 step_faa //.
+  rewrite /refines_right. rewrite -fill_app.
+  rewrite assoc. rewrite -(assoc _ spec_ctx).
+  rewrite step_faa //. rewrite fill_app.
   rewrite -[Q]elim_modal //.
   apply bi.sep_mono_r.
   apply bi.wand_intro_l.
-  rewrite (comm _ _ (l â†¦â‚› _)%I).
+  rewrite (comm _ _ (l â†¦â‚› _)%I) assoc.
+  rewrite (comm _ _ (l â†¦â‚› _)%I) -assoc.
   rewrite HQ. by apply bi.wand_elim_r.
 Qed.
 
 Tactic Notation "tp_faa" constr(j) :=
   iStartProof;
-  with_spec_ctx ltac:(fun _ =>
-      eapply (tac_tp_faa j);
-          [iSolveTC || fail "tp_faa: cannot eliminate modality in the goal"
-          |solve_ndisj || fail "tp_faa: cannot prove 'nclose specN âŠ† ?'"
-          |iAssumptionCore || fail "tp_faa: cannot find spec_ctx" (* spec_ctx *)
-          |iAssumptionCore || fail "tp_faa: cannot find '" j " â¤‡ ?'"
-          |tp_bind_helper (* e = K'[FAA _ _ _] *)
-          |iSolveTC (* IntoVal *)
-          |iAssumptionCore || fail "tp_faa: cannot find '? â†¦ ?'"
-          |simpl;reflexivity || fail "tp_faa: this should not happen"
-          |pm_reduce (* new goal *)]).
-
-
-Lemma tac_tp_fork `{relocG Î£} j Î”1 E1 i1 i2 p K' e enew e' Q :
+  eapply (tac_tp_faa j);
+  [iSolveTC || fail "tp_faa: cannot eliminate modality in the goal"
+  |solve_ndisj || fail "tp_faa: cannot prove 'nclose specN âŠ† ?'"
+  |iAssumptionCore || fail "tp_faa: cannot find the RHS '" j "'"
+  |tp_bind_helper (* e = K'[FAA _ _ _] *)
+  |iSolveTC (* IntoVal *)
+  |iAssumptionCore || fail "tp_faa: cannot find '? â†¦ ?'"
+  |simpl;reflexivity || fail "tp_faa: this should not happen"
+  |pm_reduce (* new goal *)].
+
+
+Lemma tac_tp_fork `{relocG Î£} k Î”1 E1 i1 K' e enew e' Q :
   (âˆ€ P, ElimModal True false false (|={E1}=> P) P Q Q) â†’
   nclose specN âŠ† E1 â†’
-  envs_lookup i1 Î”1 = Some (p, spec_ctx) â†’
-  envs_lookup i2 Î”1 = Some (false, j â¤‡ e)%I â†’
+  envs_lookup i1 Î”1 = Some (false, refines_right k e)%I â†’
   e = fill K' (Fork e') â†’
   enew = fill K' #() â†’
-  match envs_simple_replace i2 false
-      (Esnoc Enil i2 (j â¤‡ fill K' #())) Î”1 with
-  | Some Î”2 => envs_entails Î”2 (âˆ€ (j' : nat), j' â¤‡ e' -âˆ— Q)%I
+  match envs_simple_replace i1 false
+      (Esnoc Enil i1 (refines_right k (fill K' #()))) Î”1 with
+  | Some Î”2 => envs_entails Î”2 (âˆ€ k', refines_right k' e' -âˆ— Q)%I
   | None => False
   end â†’
   envs_entails Î”1 Q.
 Proof.
-  rewrite envs_entails_eq. intros ????->-> HQ.
-  rewrite -(idemp bi_and (of_envs Î”1)).
-  rewrite {1}(envs_lookup_sound' Î”1 false i1); last by eassumption.
-  rewrite bi.sep_elim_l /=.
-  enough (spec_ctx âˆ— of_envs Î”1 -âˆ— Q) as Hq.
-  { rewrite -Hq.
-    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). }
+  rewrite envs_entails_eq. intros ???->-> HQ.
   destruct (envs_simple_replace _ _ _ _) as [Î”2|] eqn:HÎ”2; last done.
-  rewrite (envs_simple_replace_sound Î”1 Î”2 i2) //; simpl.
+  rewrite (envs_simple_replace_sound Î”1 Î”2 i1) //; simpl.
   rewrite right_id.
-  rewrite (assoc _ spec_ctx (j â¤‡ _)%I).
-  rewrite step_fork //.
+  rewrite /refines_right. rewrite -fill_app.
+  rewrite step_fork //. rewrite fill_app.
   rewrite -[Q]elim_modal //.
   apply bi.sep_mono_r.
   apply bi.wand_intro_l.
   rewrite bi.sep_exist_r.
   apply bi.exist_elim. intros j'.
-  rewrite (comm _ (j â¤‡ _)%I (j' â¤‡ _)%I).
+  (* rewrite (comm _ (j â¤‡ _)%I (j' â¤‡ _)%I). *)
+  rewrite (comm _ _ (spec_ctx âˆ— j' â¤‡ e')%I).
   rewrite -assoc.
   rewrite bi.wand_elim_r.
-  rewrite HQ.
-  rewrite (bi.forall_elim j').
+  rewrite HQ. rewrite /refines_right.
+  rewrite (bi.forall_elim (RefId j' [])) /=.
   by rewrite bi.wand_elim_r.
 Qed.
 
 Tactic Notation "tp_fork" constr(j) :=
   iStartProof;
-  with_spec_ctx ltac:(fun _ =>
-      eapply (tac_tp_fork j);
-          [iSolveTC || fail "tp_fork: cannot eliminate modality in the goal"
-          |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
-          |simpl; reflexivity || fail "tp_fork: this should not happen"
-          |pm_reduce (* new goal *)]).
+  eapply (tac_tp_fork j);
+  [iSolveTC || fail "tp_fork: cannot eliminate modality in the goal"
+  |solve_ndisj || fail "tp_fork: cannot prove 'nclose specN âŠ† ?'"
+  |iAssumptionCore || fail "tp_fork: cannot find the RHS '" j "'"
+  |tp_bind_helper
+  |simpl; reflexivity || fail "tp_fork: this should not happen"
+  |pm_reduce (* new goal *)].
 
 Tactic Notation "tp_fork" constr(j) "as" ident(j') constr(H) :=
   iStartProof;
-  with_spec_ctx ltac:(fun _ =>
-      eapply (tac_tp_fork j);
-          [iSolveTC || fail "tp_fork: cannot eliminate modality in the goal"
-          |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
-          |simpl; reflexivity || fail "tp_fork: this should not happen"
-          |pm_reduce;
-           (iIntros (j') || fail 1 "tp_fork: " j' " not fresh ");
-           (iIntros H || fail 1 "tp_fork: " H " not fresh")
-(* new goal *)]).
+  eapply (tac_tp_fork j);
+  [iSolveTC || fail "tp_fork: cannot eliminate modality in the goal"
+  |solve_ndisj || fail "tp_fork: cannot prove 'nclose specN âŠ† ?'"
+  |iAssumptionCore || fail "tp_fork: cannot find the RHS '" j "'"
+  |tp_bind_helper
+  |simpl; reflexivity || fail "tp_fork: this should not happen"
+  |pm_reduce;
+   (iIntros (j') || fail 1 "tp_fork: " j' " not fresh ");
+   (iIntros H || fail 1 "tp_fork: " H " not fresh")
+(* new goal *)].
 
 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 i1 i2 p K' e e' v Q :
+Lemma tac_tp_alloc `{relocG Î£} k Î”1 E1 i1 K' e e' v Q :
   (âˆ€ P, ElimModal True false false (|={E1}=> P) P Q Q) â†’
   nclose specN âŠ† E1 â†’
-  envs_lookup i1 Î”1 = Some (p, spec_ctx) â†’
-  envs_lookup i2 Î”1 = Some (false, j â¤‡ e)%I â†’
+  envs_lookup i1 Î”1 = Some (false, refines_right k e)%I â†’
   e = fill K' (ref e') â†’
   IntoVal e' v â†’
   (* TODO use match here as well *)
   (âˆ€ l : loc, âˆƒ Î”2,
-    envs_simple_replace i2 false
-       (Esnoc Enil i2 (j â¤‡ fill K' #l)) Î”1 = Some Î”2 âˆ§
+    envs_simple_replace i1 false
+       (Esnoc Enil i1 (refines_right k (fill K' #l))) Î”1 = Some Î”2 âˆ§
     (envs_entails Î”2 ((l â†¦â‚› v) -âˆ— Q)%I)) â†’
   envs_entails Î”1 Q.
 Proof.
-  rewrite envs_entails_eq. intros ? ??? Hfill <- HQ.
-  rewrite -(idemp bi_and (of_envs Î”1)).
-  rewrite {1}(envs_lookup_sound' Î”1 false i1); last by eassumption.
-  rewrite bi.sep_elim_l /=.
-  enough (spec_ctx âˆ— of_envs Î”1 -âˆ— Q) as Hq.
-  { rewrite -Hq.
-    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). }
-  rewrite (envs_lookup_sound' Î”1 false i2); last by eassumption.
-  rewrite Hfill assoc /=.
+  rewrite envs_entails_eq. intros ??? Hfill <- HQ.
+  rewrite (envs_lookup_sound' Î”1 false i1); last by eassumption.
+  rewrite /refines_right.
+  rewrite Hfill -fill_app /=.
   rewrite step_alloc //.
   rewrite -[Q]elim_modal //.
   apply bi.sep_mono_r, bi.wand_intro_l.
   rewrite bi.sep_exist_r.
   apply bi.exist_elim=> l.
   destruct (HQ l) as (Î”2 & HÎ”2 & HQ').
-  rewrite (envs_simple_replace_sound' _ _ i2 _ _ HÎ”2).
-  rewrite (comm _ (j â¤‡ _)%I (l â†¦â‚› _)%I).
-  rewrite -assoc /= right_id.
+  rewrite (envs_simple_replace_sound' _ _ i1 _ _ HÎ”2) /=.
+  rewrite HQ' right_id.
+  rewrite /refines_right fill_app.
+  rewrite (comm _ _ (l â†¦â‚› _)%I).
+  rewrite assoc.
+  rewrite (comm _ _ (l â†¦â‚› _)%I).
+  rewrite -(assoc _ (l â†¦â‚› _)%I spec_ctx _). rewrite -assoc.
   rewrite bi.wand_elim_r.
-  rewrite HQ'.
   by rewrite bi.wand_elim_r.
 Qed.
 
@@ -578,97 +485,95 @@ Tactic Notation "tp_alloc" constr(j) "as" ident(l) constr(H) :=
         [ reduction.pm_reflexivity
         | (iIntros H; tp_normalise j) || fail 1 "tp_alloc:" H "not correct intro pattern" ] in
   iStartProof;
-  with_spec_ctx ltac:(fun _ =>
-      eapply (tac_tp_alloc j);
-        [iSolveTC || fail "tp_alloc: cannot eliminate modality in the goal"
-        |solve_ndisj || fail "tp_alloc: cannot prove 'nclose specN âŠ† ?'"
-        |iAssumptionCore || fail "tp_alloc: cannot find spec_ctx" (* spec_ctx *)
-        |iAssumptionCore || fail "tp_alloc: cannot find '" j " â¤‡ ?'"
-        |tp_bind_helper
-        |iSolveTC || fail "tp_alloc: expressions is not a value"
-        |finish ()
-(* new goal *)]).
+  eapply (tac_tp_alloc j);
+  [iSolveTC || fail "tp_alloc: cannot eliminate modality in the goal"
+  |solve_ndisj || fail "tp_alloc: cannot prove 'nclose specN âŠ† ?'"
+  |iAssumptionCore || fail "tp_alloc: cannot find the RHS '" j "'"
+  |tp_bind_helper
+  |iSolveTC || fail "tp_alloc: expressions is not a value"
+  |finish ()
+(* new goal *)].
 
 Tactic Notation "tp_alloc" constr(j) "as" ident(j') :=
   let H := iFresh in tp_alloc j as j' H.
 
 
-(*
-(**************************)
-(* tp_apply *)
-
-Fixpoint print_sel (ss : list sel_pat) (s : string) :=
-  match ss with
-  | nil => s
-  | SelPure :: ss' => (String "%" (String " " (print_sel ss' s)))
-  | SelPersistent :: ss' =>  (String "#" (print_sel ss' s))
-  | SelSpatial :: ss' => (* no clue :( *) (print_sel ss' s)
-  | SelIdent (INamed n) :: ss' => append n (String " " (print_sel ss' s))
-  | SelIdent (IAnon _) :: ss' => String "?" (String " " (print_sel ss' s))
-  (* wat to do with the index? *)
-  end.
-
-Ltac print_sel ss :=
-  lazymatch type of ss with
-  | list sel_pat => eval vm_compute in (print_sel ss "")
-  | string => ss
-  end.
-
-Definition appP (ss : option (list sel_pat)) (Hj Hs : string) :=
-  match ss with
-  | Some ss' => cons (SelIdent Hs) (app ss' [SelIdent Hj])
-  | None => cons (SelIdent Hs) [SelIdent Hj]
-  end.
-
-Definition add_elim_pat (pat : string) (Hj : string) :=
-  match pat with
-  | EmptyString => Hj
-  | _ => append (String "[" (append Hj (String " " pat))) "]"
-  end.
-
-Tactic Notation "tp_apply" constr(j) open_constr(lem) "with" constr(Hs) "as" constr(Hr) :=
-  iStartProof;
-  let rec find Î“ j :=
-    match Î“ with
-    | Esnoc ?Î“ (IAnon _) ?P =>
-      find Î“ j
-    | Esnoc ?Î“ (INamed ?Hj) ?P =>
-      lazymatch P with
-      | (j â¤‡ _)%I => Hj
-      | _ => find Î“ j
-      end
-    | Enil => fail 2 "tp_apply: cannot find " j " â¤‡ _ "
-    | _ => fail 2 "tp_apply: unknown error in find"
-    end in
-  let rec findSpec Î“p Î“s :=
-    match Î“p with
-    | Esnoc ?Î“ (IAnon _) _ => findSpec Î“ Î“s
-    | Esnoc ?Î“ (INamed ?Hspec) ?P =>
-      lazymatch P with
-      | (spec_ctx _)%I => Hspec
-      | _ => findSpec Î“ Î“s
-      end
-    | Enil =>
-      match Î“s with
-      | Enil => fail 2 "tp_apply: cannot find spec_ctx _"
-      | _ => findSpec Î“s Enil
-      end
-    | _ => fail 2 "tp_apply: unknown error in findSpec"
-    end in
-  match goal with
-  | |- envs_entails (Envs ?Î“p ?Î“s) ?Q =>
-    let Hj := (find Î“s j) in
-    let Hspec := findSpec Î“p Î“s in
-    let pat := eval vm_compute in (appP (sel_pat.parse Hs) Hj Hspec) in
-    let pats := print_sel pat in
-    let elim_pats := eval vm_compute in (add_elim_pat Hr Hj) in
-    iMod (lem with pats) as elim_pats; first try by solve_ndisj
-  | _ => fail "tp_apply: cannot parse the context"
-  end.
-
-Tactic Notation "tp_apply" constr(j) open_constr(lem) "with" constr(Hs) := tp_apply j lem with Hs as "".
-
-Tactic Notation "tp_apply" constr(j) open_constr(lem) "as" constr(Hr) := tp_apply j lem with "" as Hr.
-
-Tactic Notation "tp_apply" constr(j) open_constr(lem) := tp_apply j lem with "" as "".
-*)
+(* *)
+(* (**************************) *)
+(* (* tp_apply *) *)
+
+(* Fixpoint print_sel (ss : list sel_pat) (s : string) := *)
+(*   match ss with *)
+(*   | nil => s *)
+(*   | SelPure :: ss' => (String "%" (String " " (print_sel ss' s))) *)
+(*   | SelPersistent :: ss' =>  (String "#" (print_sel ss' s)) *)
+(*   | SelSpatial :: ss' => (* no clue :( *) (print_sel ss' s) *)
+(*   | SelIdent (INamed n) :: ss' => append n (String " " (print_sel ss' s)) *)
+(*   | SelIdent (IAnon _) :: ss' => String "?" (String " " (print_sel ss' s)) *)
+(*   (* wat to do with the index? *) *)
+(*   end. *)
+
+(* Ltac print_sel ss := *)
+(*   lazymatch type of ss with *)
+(*   | list sel_pat => eval vm_compute in (print_sel ss "") *)
+(*   | string => ss *)
+(*   end. *)
+
+(* Definition appP (ss : option (list sel_pat)) (Hj Hs : string) := *)
+(*   match ss with *)
+(*   | Some ss' => cons (SelIdent Hs) (app ss' [SelIdent Hj]) *)
+(*   | None => cons (SelIdent Hs) [SelIdent Hj] *)
+(*   end. *)
+
+(* Definition add_elim_pat (pat : string) (Hj : string) := *)
+(*   match pat with *)
+(*   | EmptyString => Hj *)
+(*   | _ => append (String "[" (append Hj (String " " pat))) "]" *)
+(*   end. *)
+
+(* Tactic Notation "tp_apply" constr(j) open_constr(lem) "with" constr(Hs) "as" constr(Hr) := *)
+(*   iStartProof; *)
+(*   let rec find Î“ j := *)
+(*     match Î“ with *)
+(*     | Esnoc ?Î“ (IAnon _) ?P => *)
+(*       find Î“ j *)
+(*     | Esnoc ?Î“ (INamed ?Hj) ?P => *)
+(*       lazymatch P with *)
+(*       | (j â¤‡ _)%I => Hj *)
+(*       | _ => find Î“ j *)
+(*       end *)
+(*     | Enil => fail 2 "tp_apply: cannot find " j " â¤‡ _ " *)
+(*     | _ => fail 2 "tp_apply: unknown error in find" *)
+(*     end in *)
+(*   let rec findSpec Î“p Î“s := *)
+(*     match Î“p with *)
+(*     | Esnoc ?Î“ (IAnon _) _ => findSpec Î“ Î“s *)
+(*     | Esnoc ?Î“ (INamed ?Hspec) ?P => *)
+(*       lazymatch P with *)
+(*       | (spec_ctx _)%I => Hspec *)
+(*       | _ => findSpec Î“ Î“s *)
+(*       end *)
+(*     | Enil => *)
+(*       match Î“s with *)
+(*       | Enil => fail 2 "tp_apply: cannot find spec_ctx _" *)
+(*       | _ => findSpec Î“s Enil *)
+(*       end *)
+(*     | _ => fail 2 "tp_apply: unknown error in findSpec" *)
+(*     end in *)
+(*   match goal with *)
+(*   | |- envs_entails (Envs ?Î“p ?Î“s) ?Q => *)
+(*     let Hj := (find Î“s j) in *)
+(*     let Hspec := findSpec Î“p Î“s in *)
+(*     let pat := eval vm_compute in (appP (sel_pat.parse Hs) Hj Hspec) in *)
+(*     let pats := print_sel pat in *)
+(*     let elim_pats := eval vm_compute in (add_elim_pat Hr Hj) in *)
+(*     iMod (lem with pats) as elim_pats; first try by solve_ndisj *)
+(*   | _ => fail "tp_apply: cannot parse the context" *)
+(*   end. *)
+
+(* Tactic Notation "tp_apply" constr(j) open_constr(lem) "with" constr(Hs) := tp_apply j lem with Hs as "". *)
+
+(* Tactic Notation "tp_apply" constr(j) open_constr(lem) "as" constr(Hr) := tp_apply j lem with "" as Hr. *)
+
+(* Tactic Notation "tp_apply" constr(j) open_constr(lem) := tp_apply j lem with "" as "". *)
+(* *)
diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index 8cfc9bc5f8dd3dfc8f31dc5b6b9ceb4e7cabd724..4b87c06610e32842ec3a661f6ad0feb6016f00ed 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/theories/logic/proofmode/tactics.v
@@ -16,7 +16,7 @@ Lemma tac_rel_bind_l `{!relocG Î£} e' K â„¶ E e t A :
   envs_entails â„¶ (REL e << t @ E : A).
 Proof. intros. subst. assumption. Qed.
 
-Lemma tac_rel_bind_r `{!relocG Î£} t' K â„¶ E e t A :
+Lemma tac_rel_bind_r `{!relocG Î£} (t' : expr) K â„¶ E e t A :
   t = fill K t' â†’
   envs_entails â„¶ (REL e << fill K t' @ E : A) â†’
   envs_entails â„¶ (REL e << t @ E : A).
@@ -73,10 +73,10 @@ Ltac rel_reshape_cont_l tac :=
 
 Ltac rel_reshape_cont_r tac :=
   lazymatch goal with
-  | |- envs_entails _ (refines _ _ (fill ?K ?e) _) =>
+  | |- envs_entails _ (refines _ _ (in_1 (fill ?K ?e)) _) =>
     reshape_expr e ltac:(fun K' e' =>
       tac (K' ++ K) e')
-  | |- envs_entails _ (refines _ _ ?e _) =>
+  | |- envs_entails _ (refines _ _ (in_1 ?e) _) =>
     reshape_expr e ltac:(fun K' e' => tac K' e')
   end.
 
@@ -141,7 +141,7 @@ Proof.
   - rewrite -refines_masked_l //.
 Qed.
 
-Lemma tac_rel_pure_r `{!relocG Î£} K e1 â„¶ E e e2 eres Ï• n t A :
+Lemma tac_rel_pure_r `{!relocG Î£} K e1 â„¶ E (e e2 eres : expr) Ï• n t A :
   e = fill K e1 â†’
   PureExec Ï• n e1 e2 â†’
   Ï• â†’
@@ -154,19 +154,6 @@ Proof.
   rewrite -refines_pure_r //.
 Qed.
 
-(* Tactic Notation "rel_pure_l" open_constr(ef) := *)
-(*   iStartProof; *)
-(*   (eapply tac_rel_pure_l; *)
-(*    [tac_bind_helper ef                           (** e = fill K e1' *) *)
-(*    |iSolveTC                                     (** PureClosed Ï• n e1 e2 *) *)
-(*    |try fast_done                                (** The pure condition for PureClosed *) *)
-(*    |first [left; split; reflexivity              (** Here we decide if the mask E is âŠ¤ *) *)
-(*           | right; reflexivity]                  (**    (m = n âˆ§ E = âŠ¤) âˆ¨ (m = 0) *) *)
-(*    |iSolveTC                                     (** IntoLaters *) *)
-(*    |simpl; reflexivity                           (** eres = fill K e2 *) *)
-(*    |rel_finish                                   (** new goal *)]) *)
-(*   || fail "rel_pure_l: cannot find the reduct". *)
-
 Tactic Notation "rel_pure_l" open_constr(ef) :=
   iStartProof;
   rel_reshape_cont_l ltac:(fun K e' =>
@@ -622,11 +609,11 @@ Lemma tac_rel_fork_r `{!relocG Î£} K â„¶ E e' e t eres A :
   nclose specN âŠ† E â†’
   is_closed_expr [] e' â†’
   eres = fill K #() â†’
-  envs_entails â„¶ (âˆ€ i, i â¤‡ e' -âˆ— refines E t eres A) â†’
+  envs_entails â„¶ (âˆ€ k, refines_right k e' -âˆ— refines E t eres A) â†’
   envs_entails â„¶ (refines E t e A).
 Proof.
   intros ?????. subst e eres.
-  rewrite -refines_fork_r //.
+  by rewrite -refines_fork_r //.
 Qed.
 
 Tactic Notation "rel_fork_r" ident(i) "as" constr(H) :=
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index 08b628d9b228dfb78d716f29458f77cd4f33568e..6e290564d016473c4888872eeb028e99016e085a 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -10,7 +10,7 @@ From reloc.prelude Require Import ctx_subst.
 Section rules.
   Context `{relocG Î£}.
   Implicit Types A : lrel Î£.
-  Implicit Types e t : expr.
+  Implicit Types e : expr.
   Implicit Types v w : val.
 
   Local Existing Instance pure_exec_fill.
@@ -30,9 +30,9 @@ Section rules.
   Proof.
     intros Hpure HÏ•.
     rewrite refines_eq /refines_def.
-    iIntros "IH" ; iIntros (j K) "#Hs Hj /=".
+    iIntros "IH" ; iIntros (j K) "Hs /=".
     iModIntro. wp_pures.
-    iApply fupd_wp. iApply ("IH" with "Hs Hj").
+    iApply fupd_wp. iApply ("IH" with "Hs").
   Qed.
 
   Lemma refines_masked_l E n
@@ -44,39 +44,39 @@ Section rules.
   Proof.
     intros Hpure HÏ•.
     rewrite refines_eq /refines_def.
-    iIntros "IH" ; iIntros (j K) "#Hs Hj /=".
-    iMod ("IH" with "Hs Hj") as "IH".
+    iIntros "IH" ; iIntros (j K) "Hs /=".
+    iMod ("IH" with "Hs") as "IH".
     iModIntro. by wp_pures.
   Qed.
 
-  Lemma refines_wp_l K e1 e2 A :
+  Lemma refines_wp_l K e1 t A :
     (WP e1 {{ v,
-        REL fill K (of_val v) << e2 : A }})%I -âˆ—
-    REL fill K e1 << e2 : A.
+        REL fill K (of_val v) << t : A }})%I -âˆ—
+    REL fill K e1 << t : A.
   Proof.
     rewrite refines_eq /refines_def.
     iIntros "He".
-    iIntros (j K') "#Hs Hj /=".
+    iIntros (j K') "Hs /=".
     iModIntro. iApply wp_bind.
     iApply (wp_wand with "He").
     iIntros (v) "Hv".
-    by iMod ("Hv" with "Hs Hj").
+    by iMod ("Hv" with "Hs").
   Qed.
 
-  Lemma refines_atomic_l (E : coPset) K e1 e2 A
+  Lemma refines_atomic_l (E : coPset) K e1 t A
         (Hatomic : Atomic WeaklyAtomic e1) :
    (|={âŠ¤,E}=> WP e1 @ E {{ v,
-     REL fill K (of_val v) << e2 @ E : A }})%I -âˆ—
-   REL fill K e1 << e2 : A.
+     REL fill K (of_val v) << t @ E : A }})%I -âˆ—
+   REL fill K e1 << t : A.
   Proof.
     rewrite refines_eq /refines_def.
     iIntros "Hlog".
-    iIntros (j K') "#Hs Hj /=". iModIntro.
+    iIntros (j K') "Hs /=". iModIntro.
     iApply wp_bind. iApply wp_atomic; auto.
     iMod "Hlog" as "He". iModIntro.
     iApply (wp_wand with "He").
     iIntros (v) "Hlog".
-    by iApply ("Hlog" with "Hs Hj").
+    by iApply ("Hlog" with "Hs").
   Qed.
 
   (** ** Forward reductions on the RHS *)
@@ -89,26 +89,33 @@ Section rules.
     âŠ¢ REL t << fill K' e @ E : A.
   Proof.
     rewrite refines_eq /refines_def => Hpure HÏ•.
-    iIntros "Hlog". iIntros (j K) "#Hs Hj /=".
-    tp_pure j _; auto.
-    iApply ("Hlog" with "Hs Hj").
+    iIntros "Hlog". iIntros (j K) "Hs /=".
+    tp_pures ({| tp_id := j; tp_ctx := K |}) ; auto.
+    iApply ("Hlog" with "Hs").
   Qed.
 
+  Lemma refines_right_bind k K e :
+    refines_right k (fill K e) â‰¡ refines_right (RefId (tp_id k) (K ++ tp_ctx k)) e.
+  Proof. rewrite /refines_right /=. by rewrite fill_app. Qed.
+
+  Lemma refines_right_bind' j K K' e :
+    refines_right (RefId j K) (fill K' e) â‰¡ refines_right (RefId j (K' ++ K)) e.
+  Proof. rewrite /refines_right /=. by rewrite fill_app. 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)
-                  âˆ— Î¦ v)) -âˆ—
-    (âˆ€ v, Î¦ v -âˆ— REL e1 << fill K' (of_val v) @ E : A) -âˆ—
+  Lemma refines_step_r E K' e1 e2 A :
+    (âˆ€ k, refines_right k e2 ={E}=âˆ—
+         âˆƒ v, refines_right k (of_val 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 (j K) "#Hs Hj /=".
-    rewrite -fill_app.
-    iMod ("He" $! j with "Hs Hj") as (v) "[Hj Hv]".
-    iSpecialize ("Hlog" $! v with "Hv Hs").
-    rewrite fill_app.
-    by iApply "Hlog".
+    iIntros "He".
+    iIntros (j K) "Hs /=".
+    rewrite refines_right_bind /=.
+    iMod ("He" with "Hs") as (v) "[Hs He]".
+    rewrite -refines_right_bind'.
+    iSpecialize ("He" with "Hs").
+    by iApply "He".
   Qed.
 
   Lemma refines_newproph_r E K t A
@@ -117,14 +124,10 @@ Section rules.
     -âˆ— REL t << fill K NewProph @ E : A.
   Proof.
     iIntros "Hlog".
-    pose (Î¦ := (fun w => âˆƒ (p : proph_id), âŒœw = (# p)âŒ : iProp Î£)%I).
-    iApply (refines_step_r Î¦); simpl; auto.
-    { cbv[Î¦].
-      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.
-    by iApply "Hlog".
+    iApply refines_step_r.
+    iIntros (k) "[Hs Hj]".
+    iMod (step_newproph with "[$Hs $Hj]") as (p) "Hj". done.
+    iModIntro. iExists _. iFrame "Hj". by iApply "Hlog".
   Qed.
 
   Lemma refines_resolveproph_r E K t (p : proph_id) w A
@@ -133,13 +136,23 @@ Section rules.
     -âˆ— REL t << fill K (ResolveProph #p (of_val w)) @ E : A.
   Proof.
     iIntros "Hlog".
-    pose (Î¦ := (fun w => âŒœw = #()âŒ : iProp Î£)%I).
-    iApply (refines_step_r Î¦); simpl; auto.
-    { cbv[Î¦].
-      iIntros (j K') "#Hs Hj /=".
-      iMod (step_resolveproph with "[$Hs $Hj]") as "Hj". done.
-      iModIntro. iExists _. iFrame. eauto. }
-    iIntros (v') "He'". iDestruct "He'" as %->.
+    iApply refines_step_r.
+    iIntros (k) "[Hs Hj]".
+    iMod (step_resolveproph with "[$Hs $Hj]") as "Hj". done.
+    iModIntro. iExists _. iFrame "Hj". by iApply "Hlog".
+  Qed.
+
+  Lemma refines_store_r E K l e e' v v' A
+    (Hmasked : nclose specN âŠ† E) :
+    IntoVal e' v' â†’
+    l â†¦â‚› v -âˆ—
+    (l â†¦â‚› v' -âˆ— REL e << fill K (of_val #()) @ E : A) -âˆ—
+    REL e << fill K (#l <- e') @ E : A.
+  Proof.
+    rewrite /IntoVal. iIntros (<-) "Hl Hlog".
+    iApply refines_step_r.
+    iIntros (k) "Hk". simpl.
+    tp_store k. iModIntro. iExists _. iFrame.
     by iApply "Hlog".
   Qed.
 
@@ -149,16 +162,12 @@ Section rules.
     (âˆ€ l : loc, l â†¦â‚› v -âˆ— REL t << fill K (of_val #l) @ E : A)%I
     -âˆ— REL t << fill K (ref e) @ E : A.
   Proof.
-    intros <-.
+    rewrite /IntoVal. intros <-.
     iIntros "Hlog".
-    pose (Î¦ := (fun w => âˆƒ l : loc, âŒœw = (# l)âŒ âˆ— l â†¦â‚› v)%I).
-    iApply (refines_step_r Î¦); simpl; auto.
-    { cbv[Î¦].
-      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.
-    by iApply "Hlog".
+    iApply refines_step_r.
+    iIntros (k) "Hk".
+    tp_alloc k as l "Hl".
+    iModIntro. iExists _. iFrame. by iApply "Hlog".
   Qed.
 
   Lemma refines_load_r E K l q v t A
@@ -168,32 +177,10 @@ Section rules.
     -âˆ— REL t << (fill K !#l) @ E : A.
   Proof.
     iIntros "Hl Hlog".
-    pose (Î¦ := (fun w => âŒœw = vâŒ âˆ— l â†¦â‚›{q} v)%I).
-    iApply (refines_step_r Î¦ with "[Hl]"); eauto.
-    { cbv[Î¦].
-      iIntros (j K') "#Hs Hj /=". iExists v.
-      tp_load j.
-      iFrame. eauto. }
-    iIntros (?) "[% Hl]"; subst.
-    by iApply "Hlog".
-  Qed.
-
-  Lemma refines_store_r E K l e e' v v' A
-    (Hmasked : nclose specN âŠ† E) :
-    IntoVal e' v' â†’
-    l â†¦â‚› v -âˆ—
-    (l â†¦â‚› v' -âˆ— REL e << fill K (of_val #()) @ E : A) -âˆ—
-    REL e << fill K (#l <- e') @ E : A.
-  Proof.
-    iIntros (<-) "Hl Hlog".
-    pose (Î¦ := (fun w => âŒœw = #()âŒ âˆ— l â†¦â‚› v')%I).
-    iApply (refines_step_r Î¦ with "[Hl]"); eauto.
-    { cbv[Î¦].
-      iIntros (j K') "#Hs Hj /=". iExists #().
-      tp_store j.
-      iFrame. eauto. }
-    iIntros (w) "[% Hl]"; subst.
-    by iApply "Hlog".
+    iApply refines_step_r.
+    iIntros (k) "Hk".
+    tp_load k.
+    iModIntro. iExists _. iFrame. by iApply "Hlog".
   Qed.
 
   Lemma refines_cmpxchg_fail_r E K l e1 e2 v1 v2 v t A :
@@ -206,16 +193,11 @@ Section rules.
     (l â†¦â‚› v -âˆ— REL t << fill K (of_val (v, #false)) @ E : A)
     -âˆ— REL t << fill K (CmpXchg #l e1 e2) @ E : A.
   Proof.
-    iIntros (?<-<-??) "Hl Hlog".
-    pose (Î¦ := (fun (w : val) => âŒœw = (v, #false)%VâŒ âˆ— l â†¦â‚› v)%I).
-    iApply (refines_step_r Î¦ with "[Hl]"); eauto.
-    { cbv[Î¦].
-      iIntros (j K') "#Hs Hj /=".
-      tp_cmpxchg_fail j; auto.
-      iExists _. simpl.
-      iFrame. eauto. }
-    iIntros (w) "[% Hl]"; subst.
-    by iApply "Hlog".
+    rewrite /IntoVal. iIntros (?<-<-??) "Hl Hlog".
+    iApply refines_step_r.
+    iIntros (k) "Hk".
+    tp_cmpxchg_fail k.
+    iModIntro. iExists _. iFrame. by iApply "Hlog".
   Qed.
 
   Lemma refines_cmpxchg_suc_r E K l e1 e2 v1 v2 v t A :
@@ -228,16 +210,11 @@ Section rules.
     (l â†¦â‚› v2 -âˆ— REL t << fill K (of_val (v, #true)) @ E : A)
     -âˆ— REL t << fill K (CmpXchg #l e1 e2) @ E : A.
   Proof.
-    iIntros (?<-<-??) "Hl Hlog".
-    pose (Î¦ := (fun w => âŒœw = (v, #true)%VâŒ âˆ— l â†¦â‚› v2)%I).
-    iApply (refines_step_r Î¦ with "[Hl]"); eauto.
-    { cbv[Î¦].
-      iIntros (j K') "#Hs Hj /=".
-      tp_cmpxchg_suc j; auto.
-      iExists _. simpl.
-      iFrame. eauto. }
-    iIntros (w) "[% Hl]"; subst.
-    by iApply "Hlog".
+    rewrite /IntoVal. iIntros (?<-<-??) "Hl Hlog".
+    iApply refines_step_r.
+    iIntros (k) "Hk".
+    tp_cmpxchg_suc k.
+    iModIntro. iExists _. iFrame. by iApply "Hlog".
   Qed.
 
   Lemma refines_faa_r E K l e2 (i1 i2 : Z) t A :
@@ -247,33 +224,24 @@ Section rules.
     (l â†¦â‚› #(i1+i2) -âˆ— REL t << fill K (of_val #i1) @ E : A)
     -âˆ— REL t << fill K (FAA #l e2) @ E : A.
   Proof.
-    iIntros (?<-) "Hl Hlog".
-    pose (Î¦ := (fun w => âŒœw = #i1âŒ âˆ— l â†¦â‚› #(i1+i2))%I).
-    iApply (refines_step_r Î¦ with "[Hl]"); eauto.
-    { cbv[Î¦].
-      iIntros (j K') "#Hs Hj /=".
-      tp_faa j; auto.
-      iExists #i1. simpl.
-      iFrame. eauto. }
-    iIntros (w) "[% Hl]"; subst.
-    by iApply "Hlog".
+    rewrite /IntoVal. iIntros (?<-) "Hl Hlog".
+    iApply refines_step_r.
+    iIntros (k) "Hk".
+    tp_faa k.
+    iModIntro. iExists _. iFrame. by iApply "Hlog".
   Qed.
 
   Lemma refines_fork_r E K (e t : expr) A
    (Hmasked : nclose specN âŠ† E) :
-   (âˆ€ i, i â¤‡ e -âˆ—
+   (âˆ€ k, refines_right k e -âˆ—
      REL t << fill K (of_val #()) @ E : A) -âˆ—
    REL t << fill K (Fork e) @ E : A.
   Proof.
     iIntros "Hlog".
-    pose (Î¦ := (fun (v : val) => âˆƒ i, i â¤‡ e âˆ— âŒœv = #()âŒ%V)%I).
-    iApply (refines_step_r Î¦ with "[]"); cbv[Î¦].
-    { iIntros (j K') "#Hspec Hj".
-      tp_fork j as i "Hi".
-      iModIntro. iExists #(). iFrame. eauto.
-    }
-    iIntros (v). iDestruct 1 as (i) "[Hi %]"; subst.
-    by iApply "Hlog".
+    iApply refines_step_r.
+    iIntros (k) "Hk".
+    tp_fork k as k' "Hk'".
+    iModIntro. iExists _. iFrame. by iApply "Hlog".
   Qed.
 
   (** ** Primitive structural rules *)
@@ -283,26 +251,26 @@ Section rules.
   Proof.
     rewrite refines_eq /refines_def.
     iIntros "H".
-    iIntros (j K) "#Hs Hj /=".
-    tp_fork j as i "Hi". iModIntro.
-    iSpecialize ("H" $! i [] with "Hs Hi").
+    iIntros (j K) "Hs /=".
+    tp_fork ({| tp_id := j; tp_ctx := K |}) as k' "Hk'". iModIntro.
+    simpl.
+    iSpecialize ("H" with "Hk'").
     iApply (wp_fork with "[H]").
     - iNext. iMod "H". iApply (wp_wand with "H"). eauto.
-    - iNext. iExists _. by iFrame.
+    - iNext. iExists _. rewrite /refines_right.
+      iDestruct "Hs" as "[_ $]". done.
   Qed.
 
   (** This rule is useful for proving that functions refine each other *)
-  Lemma refines_arrow_val v v' A A' :
+  Lemma refines_arrow_val (v v' : val) A A' :
     â–¡(âˆ€ v1 v2, A v1 v2 -âˆ—
       REL App v (of_val v1) << App v' (of_val v2) : A') -âˆ—
-    REL v << v' : (A â†’ A')%lrel.
+    REL (of_val v) << (of_val v') : (A â†’ A')%lrel.
   Proof.
-    rewrite /AsRecV. iIntros "#H".
-    iApply refines_spec_ctx. iIntros "Hs".
+    iIntros "#H".
     iApply refines_ret. iModIntro.
     iModIntro. iIntros (v1 v2) "HA".
     iSpecialize ("H" with "HA").
-    rewrite refines_eq /refines_def.
     by iApply "H".
   Qed.
 
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index 63bb37440faf8f1e9d34a881ef25b44ab8b4cde2..404953819d3ed2e354cb8606fb6f531aadb1c8f7 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -147,10 +147,10 @@ Section to_heap.
   Lemma to_heap_valid Ïƒ : âœ“ to_heap Ïƒ.
   Proof. intros l. rewrite lookup_fmap. by case (Ïƒ !! l). Qed.
 
-End to_heap.  
+End to_heap.
 
 Section mapsto.
-  Context `{cfgSG Î£}.
+  Context `{!cfgSG Î£}.
 
   Global Instance mapstoS_fractional l v : Fractional (Î» q, l â†¦â‚›{q} v)%I.
   Proof.
@@ -164,10 +164,13 @@ Section mapsto.
   Lemma mapstoS_agree l q1 q2 v1 v2 : l â†¦â‚›{q1} v1 -âˆ— l â†¦â‚›{q2} v2 -âˆ— âŒœv1 = v2âŒ.
   Proof.
     apply bi.wand_intro_r.
-    rewrite heapS_mapsto_eq -own_op own_valid uPred.discrete_valid. f_equiv.
-    rewrite auth_frag_op_valid -pair_op singleton_op -pair_op.
-    rewrite pair_valid singleton_valid pair_valid to_agree_op_valid_L.
-    by intros [_ [_ [=]]].
+    rewrite heapS_mapsto_eq -own_op -auth_frag_op own_valid uPred.discrete_valid.
+    f_equiv=> /=.
+    rewrite -pair_op singleton_op right_id -pair_op.
+    rewrite auth_frag_valid pair_valid.
+    intros [_ Hv]. move:Hv => /=.
+    rewrite singleton_valid.
+    by move=> [_] /to_agree_op_inv_L [->].
   Qed.
 
   Lemma mapstoS_valid l q v : l â†¦â‚›{q} v -âˆ— âœ“ q.
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index a02bc4e21dcc0aa06001945106bb3b5b394c7ac0..66c8947d8f02da6c21054e575ee7463c5e66dc2a 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -38,27 +38,15 @@ Section rules.
     erased_step (tp, Ïƒ) (<[j:=fill K e']> tp, Ïƒ').
   Proof. rewrite -(right_id_L [] (++) (<[_:=_]>_)). by apply step_insert. Qed.
 
-  Lemma nsteps_inv_r {A} n (R : A â†’ A â†’ Prop) x y :
-    relations.nsteps R (S n) x y â†’ âˆƒ z, relations.nsteps R n x z âˆ§ R z y.
-  Proof.
-    revert x y; induction n; intros x y.
-    - inversion 1; subst.
-      match goal with H : relations.nsteps _ 0 _ _ |- _ => inversion H end; subst.
-      eexists; repeat econstructor; eauto.
-    - inversion 1; subst.
-      edestruct IHn as [z [? ?]]; eauto.
-      exists z; split; eauto using relations.nsteps_l.
-  Qed.
-
   (** * Main rules *)
   (** Pure reductions *)
   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}=âˆ— spec_ctx âˆ— j â¤‡ fill K e'.
   Proof.
-    iIntros (HP Hex ?) "[#Hspec Hj]".
+    iIntros (HP Hex ?) "[#Hspec Hj]". iFrame "Hspec".
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=.
     iDestruct "Hspec" as (Ï) "Hspec".
     iInv specN as (tp Ïƒ) ">[Hown Hrtc]" "Hclose".
@@ -102,9 +90,9 @@ Section rules.
   Lemma step_newproph E j K :
     nclose specN âŠ† E â†’
     spec_ctx âˆ— j â¤‡ fill K NewProph ={E}=âˆ—
-    âˆƒ (p : proph_id), j â¤‡ fill K #p.
+    âˆƒ (p : proph_id), spec_ctx âˆ— j â¤‡ fill K #p.
   Proof.
-    iIntros (?) "[#Hinv Hj]".
+    iIntros (?) "[#Hinv Hj]". iFrame "Hinv".
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=.
     iDestruct "Hinv" as (Ï) "Hinv".
     iInv specN as (tp Ïƒ) ">[Hown %]" "Hclose".
@@ -123,9 +111,9 @@ Section rules.
   Lemma step_resolveproph E j K (p : proph_id) w :
     nclose specN âŠ† E â†’
     spec_ctx âˆ— j â¤‡ fill K (ResolveProph #p (of_val w)) ={E}=âˆ—
-    j â¤‡ fill K #().
+    spec_ctx âˆ— j â¤‡ fill K #().
   Proof.
-    iIntros (?) "[#Hinv Hj]".
+    iIntros (?) "[#Hinv Hj]". iFrame "Hinv".
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=.
     iDestruct "Hinv" as (Ï) "Hinv".
     iInv specN as (tp Ïƒ) ">[Hown %]" "Hclose".
@@ -144,9 +132,9 @@ Section rules.
   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, spec_ctx âˆ— j â¤‡ fill K (#l) âˆ— l â†¦â‚› v.
   Proof.
-    iIntros (<-?) "[#Hinv Hj]".
+    iIntros (<-?) "[#Hinv Hj]". iFrame "Hinv".
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=.
     iDestruct "Hinv" as (Ï) "Hinv".
     iInv specN as (tp Ïƒ) ">[Hown %]" "Hclose".
@@ -172,9 +160,9 @@ Section rules.
   Lemma step_load E j K l q v:
     nclose specN âŠ† E â†’
     spec_ctx âˆ— j â¤‡ fill K (!#l) âˆ— l â†¦â‚›{q} v
-    ={E}=âˆ— j â¤‡ fill K (of_val v) âˆ— l â†¦â‚›{q} v.
+    ={E}=âˆ— spec_ctx âˆ— j â¤‡ fill K (of_val v) âˆ— l â†¦â‚›{q} v.
   Proof.
-    iIntros (?) "(#Hinv & Hj & Hl)".
+    iIntros (?) "(#Hinv & Hj & Hl)". iFrame "Hinv".
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
     iDestruct "Hinv" as (Ï) "Hinv".
     rewrite heapS_mapsto_eq /heapS_mapsto_def /=.
@@ -196,9 +184,9 @@ Section rules.
     IntoVal e v â†’
     nclose specN âŠ† E â†’
     spec_ctx âˆ— j â¤‡ fill K (#l <- e) âˆ— l â†¦â‚› v'
-    ={E}=âˆ— j â¤‡ fill K #() âˆ— l â†¦â‚› v.
+    ={E}=âˆ— spec_ctx âˆ— j â¤‡ fill K #() âˆ— l â†¦â‚› v.
   Proof.
-    iIntros (<-?) "(#Hinv & Hj & Hl)".
+    iIntros (<-?) "(#Hinv & Hj & Hl)". iFrame "Hinv".
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
     iDestruct "Hinv" as (Ï) "Hinv".
     rewrite heapS_mapsto_eq /heapS_mapsto_def /=.
@@ -231,9 +219,9 @@ Section rules.
     vals_compare_safe v' v1 â†’
     v' â‰  v1 â†’
     spec_ctx âˆ— j â¤‡ fill K (CmpXchg #l e1 e2) âˆ— l â†¦â‚›{q} v'
-    ={E}=âˆ— j â¤‡ fill K (v', #false)%V âˆ— l â†¦â‚›{q} v'.
+    ={E}=âˆ— spec_ctx âˆ— j â¤‡ fill K (v', #false)%V âˆ— l â†¦â‚›{q} v'.
   Proof.
-    iIntros (<-<-???) "(#Hinv & Hj & Hl)".
+    iIntros (<-<-???) "(#Hinv & Hj & Hl)". iFrame "Hinv".
     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".
@@ -258,9 +246,9 @@ Section rules.
     vals_compare_safe v1' v1 â†’
     v1' = v1 â†’
     spec_ctx âˆ— j â¤‡ fill K (CmpXchg #l e1 e2) âˆ— l â†¦â‚› v1'
-    ={E}=âˆ— j â¤‡ fill K (v1', #true)%V âˆ— l â†¦â‚› v2.
+    ={E}=âˆ— spec_ctx âˆ— j â¤‡ fill K (v1', #true)%V âˆ— l â†¦â‚› v2.
   Proof.
-    iIntros (<-<-???) "(#Hinv & Hj & Hl)"; subst.
+    iIntros (<-<-???) "(#Hinv & Hj & Hl)"; subst. iFrame "Hinv".
     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".
@@ -289,9 +277,9 @@ Section rules.
     IntoVal e1 #i2 â†’
     nclose specN âŠ† E â†’
     spec_ctx âˆ— j â¤‡ fill K (FAA #l e1) âˆ— l â†¦â‚› #i1
-    ={E}=âˆ— j â¤‡ fill K #i1 âˆ— l â†¦â‚› #(i1+i2).
+    ={E}=âˆ— spec_ctx âˆ— j â¤‡ fill K #i1 âˆ— l â†¦â‚› #(i1+i2).
   Proof.
-    iIntros (<-?) "(#Hinv & Hj & Hl)"; subst.
+    iIntros (<-?) "(#Hinv & Hj & Hl)"; subst. iFrame "Hinv".
     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".
@@ -318,9 +306,10 @@ Section rules.
   (** Fork *)
   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', (spec_ctx âˆ— j â¤‡ fill K #()) âˆ— (spec_ctx âˆ— j' â¤‡ e).
   Proof.
-    iIntros (?) "[#Hspec Hj]".
+    iIntros (?) "[#Hspec Hj]". iFrame "Hspec".
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
     iDestruct "Hspec" as (Ï) "Hspec".
     iInv specN as (tp Ïƒ) ">[Hown %]" "Hclose".
diff --git a/theories/tests/proofmode_tests.v b/theories/tests/proofmode_tests.v
index c1dd406875cccfefbf8667d905f5f36a6be89843..911cd662c49480b332f51c44f8e33597d94fdf37 100644
--- a/theories/tests/proofmode_tests.v
+++ b/theories/tests/proofmode_tests.v
@@ -7,7 +7,7 @@ Context `{relocG Î£}.
 
 Definition EqI : lrel Î£ := LRel (Î» v1 v2, âŒœv1 = v2âŒ)%I.
 (* Pure reductions *)
-Lemma test1 A P t :
+Lemma test1 A P (t: expr) :
   â–· P -âˆ—
   (P -âˆ— REL #4 << t : A) -âˆ—
   REL (#2 + #2) << (Î»: <>, t) #() : A.
diff --git a/theories/tests/tp_tests.v b/theories/tests/tp_tests.v
index 0b7077e433229ccf84963485b40b20229bafe9d4..442d4fb3d5c85b34fbcd4aa4ae6ad3c922cddc14 100644
--- a/theories/tests/tp_tests.v
+++ b/theories/tests/tp_tests.v
@@ -3,81 +3,81 @@ From reloc.logic Require Export spec_rules proofmode.spec_tactics.
 Set Default Proof Using "Type".
 Import lang.
 
-Section test.
-Context `{relocG Î£}.
+(* Section test. *)
+(* Context `{relocG Î£}. *)
 
-(* store, load, and some pure reductions *)
-Lemma test1 E1 j K (l : loc) (n : nat) :
-  nclose specN âŠ† E1 â†’
-  spec_ctx -âˆ—
-  j â¤‡ fill K ((Î»: "x", #l <- "x" + #1) !#l)%E -âˆ—
-  l â†¦â‚› #n
-  ={E1}=âˆ— l â†¦â‚› #(n+1) âˆ— j â¤‡ fill K #().
-Proof.
-  iIntros (?) "#? Hj Hl".
-  tp_load j.
-  tp_pures j.
-  tp_store j. by iFrame.
-Qed.
+(* (* store, load, and some pure reductions *) *)
+(* Lemma test1 E1 j K (l : loc) (n : nat) : *)
+(*   nclose specN âŠ† E1 â†’ *)
+(*   spec_ctx -âˆ— *)
+(*   j â¤‡ fill K ((Î»: "x", #l <- "x" + #1) !#l)%E -âˆ— *)
+(*   l â†¦â‚› #n *)
+(*   ={E1}=âˆ— l â†¦â‚› #(n+1) âˆ— j â¤‡ fill K #(). *)
+(* Proof. *)
+(*   iIntros (?) "#? Hj Hl". *)
+(*   tp_load j. *)
+(*   tp_pures j. *)
+(*   tp_store j. by iFrame. *)
+(* Qed. *)
 
-(* CAS *)
-Lemma test2 E1 j K (l : loc) (n : nat) :
-  nclose specN âŠ† E1 â†’
-  spec_ctx -âˆ—
-  j â¤‡ fill K (CAS #l #2 #n;; CAS #l #3 (#n*#2)) -âˆ—
-  l â†¦â‚› #3
-  ={E1}=âˆ— l â†¦â‚› #(n*2) âˆ— j â¤‡ fill K #true.
-Proof.
-  iIntros (?) "#? Hj Hl".
-  tp_cmpxchg_fail j.
-  tp_pures j.
-  tp_cmpxchg_suc j.
-  tp_pures j. by iFrame.
-Qed.
+(* (* CAS *) *)
+(* Lemma test2 E1 j K (l : loc) (n : nat) : *)
+(*   nclose specN âŠ† E1 â†’ *)
+(*   spec_ctx -âˆ— *)
+(*   j â¤‡ fill K (CAS #l #2 #n;; CAS #l #3 (#n*#2)) -âˆ— *)
+(*   l â†¦â‚› #3 *)
+(*   ={E1}=âˆ— l â†¦â‚› #(n*2) âˆ— j â¤‡ fill K #true. *)
+(* Proof. *)
+(*   iIntros (?) "#? Hj Hl". *)
+(*   tp_cmpxchg_fail j. *)
+(*   tp_pures j. *)
+(*   tp_cmpxchg_suc j. *)
+(*   tp_pures j. by iFrame. *)
+(* Qed. *)
 
-(* fork *)
-Lemma test3 E1 j e K (l : loc) (n : nat) :
-  nclose specN âŠ† E1 â†’
-  spec_ctx -âˆ—
-  j â¤‡ fill K (Fork e)
-  ={E1}=âˆ— âˆƒ i, i â¤‡ e âˆ— j â¤‡ fill K #().
-Proof.
-  iIntros (?) "#? Hj".
-  tp_fork j as i. eauto with iFrame.
-Qed.
+(* (* fork *) *)
+(* Lemma test3 E1 j e K (l : loc) (n : nat) : *)
+(*   nclose specN âŠ† E1 â†’ *)
+(*   spec_ctx -âˆ— *)
+(*   j â¤‡ fill K (Fork e) *)
+(*   ={E1}=âˆ— âˆƒ i, i â¤‡ e âˆ— j â¤‡ fill K #(). *)
+(* Proof. *)
+(*   iIntros (?) "#? Hj". *)
+(*   tp_fork j as i. eauto with iFrame. *)
+(* Qed. *)
 
-(* alloc *)
-Lemma test4 E1 j K (n : nat) :
-  nclose specN âŠ† E1 â†’
-  spec_ctx -âˆ—
-  j â¤‡ fill K (ref #3)
-  ={E1}=âˆ— âˆƒ l, l â†¦â‚› #3 âˆ— j â¤‡ fill K #l.
-Proof.
-  iIntros (?) "#? Hj".
-  tp_alloc j as l "Hl".
-  iExists l. by iFrame.
-Qed.
+(* (* alloc *) *)
+(* Lemma test4 E1 j K (n : nat) : *)
+(*   nclose specN âŠ† E1 â†’ *)
+(*   spec_ctx -âˆ— *)
+(*   j â¤‡ fill K (ref #3) *)
+(*   ={E1}=âˆ— âˆƒ l, l â†¦â‚› #3 âˆ— j â¤‡ fill K #l. *)
+(* Proof. *)
+(*   iIntros (?) "#? Hj". *)
+(*   tp_alloc j as l "Hl". *)
+(*   iExists l. by iFrame. *)
+(* Qed. *)
 
 
-End test.
+(* End test. *)
 
-(* Section test2. *)
-(* Context `{logrelG Î£}. *)
-(* (* 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) *)
-(*     ={E}=âˆ— j â¤‡ fill K #() âˆ— l â†¦â‚› #false). *)
+(* (* Section test2. *) *)
+(* (* Context `{logrelG Î£}. *) *)
+(* (* (* 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) *) *)
+(* (*     ={E}=âˆ— j â¤‡ fill K #() âˆ— l â†¦â‚› #false). *) *)
 
-(* Theorem test_apply E Ï j (b : bool) K l: *)
-(*   nclose specN âŠ† E â†’ *)
-(*   spec_ctx -âˆ—  *)
-(*   l â†¦â‚› #b -âˆ— j â¤‡ fill K (App #() #l) *)
-(*   -âˆ— |={E}=> True. *)
-(* Proof. *)
-(*   iIntros (?) "#Hs Hst Hj". *)
-(*   tp_apply j steps_release_test with "Hst" as "Hl". *)
-(*   done. *)
-(* Qed. *)
+(* (* Theorem test_apply E Ï j (b : bool) K l: *) *)
+(* (*   nclose specN âŠ† E â†’ *) *)
+(* (*   spec_ctx -âˆ—  *) *)
+(* (*   l â†¦â‚› #b -âˆ— j â¤‡ fill K (App #() #l) *) *)
+(* (*   -âˆ— |={E}=> True. *) *)
+(* (* Proof. *) *)
+(* (*   iIntros (?) "#Hs Hst Hj". *) *)
+(* (*   tp_apply j steps_release_test with "Hst" as "Hl". *) *)
+(* (*   done. *) *)
+(* (* Qed. *) *)
 
-(* End test2. *)
+(* (* End test2. *) *)
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 46fcd4df9540b218d82e9389670fdd39c75463a3..f4c96c7553132cc6fe03fa712f19dd4e617455f0 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -92,7 +92,6 @@ 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. 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)).
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 8093802248f6da1007a76df7feafb814a559c784..4506b34ce0abb34c5bfcb4fdbc23d6e3680668c6 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -74,7 +74,7 @@ Proof.
   iModIntro. iIntros (?). iApply Hlog.
 Qed.
 
-Lemma refines_sound Î£ `{relocPreG Î£} e e' Ï„ :
+Lemma refines_sound Î£ `{relocPreG Î£} (e e': expr) Ï„ :
   (âˆ€ `{relocG Î£} Î”, âŠ¢ REL e << e' : (interp Ï„ Î”)) â†’
   âˆ… âŠ¨ e â‰¤ctxâ‰¤ e' : Ï„.
 Proof.