diff --git a/theories/examples/par.v b/theories/examples/par.v
index 587f2560af40b1a09c91701b80533f5fd0cd177e..63abc2a666c4e64ce1bddad03baaffdf61e720e9 100644
--- a/theories/examples/par.v
+++ b/theories/examples/par.v
@@ -90,12 +90,10 @@ Section rules.
     rel_bind_l (spawn _). iApply refines_wp_l.
     iApply (spawn_spec N (λ _, refines_right k #())%I with "[He1 Hk]").
     - wp_pures. wp_bind e1.
-      rewrite refines_eq /refines_def.
-      iDestruct "Hk" as "[#Hs Hj]".
-      iMod ("He1" with "[$Hs $Hj]") as "He1".
+      rewrite refines_eq /refines_def /=.
+      iMod ("He1" with "Hk") as "He1".
       iApply (wp_wand with "He1").
       iIntros (?)  "P". wp_pures.
-      iFrame "Hs".
       by iDestruct "P" as (v') "[? [-> ->]]".
     - iNext. iIntros (l) "hndl". iSimpl.
       rel_pures_l. rel_bind_l e2.
@@ -108,6 +106,15 @@ Section rules.
       rel_values.
   Qed.
 
+  Lemma refines_right_cons k' Ki K e :
+    refines_right (RefId k' (Ki::K)) e =
+    refines_right (RefId k' K) (fill_item Ki e).
+  Proof. rewrite /refines_right /= //. Qed.
+  Lemma refines_right_fill k K e :
+    refines_right k (fill K e) =
+    refines_right (RefId (tp_id k) (K ++ tp_ctx k)) e.
+  Proof. rewrite /refines_right fill_app //. Qed.
+
   Lemma par_l_1' Q K e1 e2 t :
     (REL e1 << t : ()) -∗
     (WP e2 {{ _, Q }}) -∗
@@ -124,14 +131,11 @@ Section rules.
     iApply (spawn_spec N (λ _, refines_right k (fill K #()))%I with "[He1 Hk]").
     - wp_pures. wp_bind e1.
       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.
-      rewrite /refines_right.
       iDestruct "P" as (v') "[Hj [-> ->]]".
-      iFrame "Hs". by rewrite fill_app.
+      by rewrite refines_right_fill.
     - iNext. iIntros (l) "Hl". simpl.
       rel_pures_l. rel_bind_l e2.
       iApply refines_wp_l.
@@ -256,38 +260,32 @@ Section rules.
     repeat rel_pure_r.
     tp_rec i. simpl.
     rewrite {3}refines_eq /refines_def /=.
-    iIntros (j' K).
-    set (j := {| tp_id := j'; tp_ctx := K |}).
-    iIntros "Hj". iModIntro.
+    iIntros (j) "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.
-    iDestruct "Hi" as "[#Hs Hi]".
-    iMod ("He1" $! (tp_id i)  with "[Hi]") as "He1".
-    { rewrite /refines_right -fill_app //. by iFrame. }
+    rewrite !refines_right_fill.
+    rewrite {1}refines_eq /refines_def /=.
+    iMod ("He1" with "Hi") as "He1".
     iApply (wp_wand with "He1"). iIntros (v1).
     iDestruct 1 as (v2) "[Hi Hv]". wp_pures.
     (* execute e2 *)
     rewrite refines_eq /refines_def.
-    iMod ("He2" $! (tp_id j) with "[Hj]") as "He2".
-    { rewrite /refines_right -fill_app //.
-      cbn-[fill]. iFrame "Hj". }
+    iMod ("He2" with "Hj") as "He2".
     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. }
+    rewrite !refines_right_cons /=.
+    change (RefId (tp_id i) (tp_ctx i)) with i.
+    change (RefId (tp_id j) (tp_ctx j)) with j.
     tp_pure i _.
     tp_store i.
     tp_pures j. tp_rec j.
     tp_load j.
     tp_pures j.
     iModIntro. iExists _.
-    iDestruct "Hj" as "[_ $]".
+    by iFrame.
   Qed.
 
   Lemma interchange a b c d (A B C D : lrel Σ) :
@@ -310,68 +308,58 @@ Section rules.
     tp_rec i. simpl.
     rel_rec_l. repeat rel_pure_l.
     rewrite {5}refines_eq /refines_def.
-    iIntros (j' K). simpl.
-    set (j := {| tp_id := j'; tp_ctx := K |}).
+    iIntros (j) "Hj". iModIntro.
     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 "[Hj]") as "Ha".
-      { rewrite /refines_right -fill_app //.
-        cbn-[fill]. iFrame "Hj". }
+      rewrite refines_right_fill.
+      iMod ("Ha" with "Hj") as "Ha".
       iExact "Ha".
     - iNext. iIntros (h) "Hdl". wp_pures.
       wp_bind b.
       rewrite {1}refines_eq /refines_def.
       tp_bind i b.
-      iDestruct "Hi" as "[#Hs Hi]".
-      iMod ("Hb" with "[Hi]") as "Hb".
-      { rewrite /refines_right -fill_app //; by iFrame. }
+      rewrite refines_right_fill.
+      iMod ("Hb" with "Hi") as "Hb".
       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.
-      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. }
+      rewrite !refines_right_cons /=.
+      change (RefId (tp_id i) (tp_ctx i)) with i.
+      change (RefId (tp_id j) (tp_ctx j)) with j.
       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 /=.
         tp_bind i c.
-        iMod ("Hc" with "[Hi]") as "Hc".
-        { rewrite /refines_right -fill_app //. }
+        rewrite refines_right_fill.
+        iMod ("Hc" with "Hi") as "Hc".
         iExact "Hc". }
       clear h. iIntros (h) "Hdl". wp_pures.
       wp_bind d.
       rewrite refines_eq /refines_def.
       tp_bind j d.
-      iMod ("Hd" $! (tp_id j) with "[Hj]") as "Hd".
-      { rewrite /refines_right -fill_app //.
-        iSimpl. by iFrame. }
+      rewrite refines_right_fill.
+      iMod ("Hd" with "Hj") as "Hd".
       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. }
+      rewrite !refines_right_cons /=.
+      change (RefId (tp_id i) (tp_ctx i)) with i.
+      change (RefId (tp_id j) (tp_ctx j)) with j.
       tp_pures i. tp_store i.
       tp_pures j.
       rewrite /spawn.join. tp_pures j.
       tp_load j. tp_pures j.
       iModIntro; iSplit; eauto with iFrame.
-      iDestruct "Hj" as "[_ $]".
   Qed.
 End rules.
diff --git a/theories/logic/adequacy.v b/theories/logic/adequacy.v
index ccbdcea43b67d21836d72b4922ee0992abaa978b..f1ec69944c9fb94d2e0788c8d5c5a9d92ae8806b 100644
--- a/theories/logic/adequacy.v
+++ b/theories/logic/adequacy.v
@@ -39,7 +39,7 @@ Proof.
   iSplitL.
   - iPoseProof (Hlog _) as "Hrel".
     rewrite refines_eq /refines_def /spec_ctx.
-    iApply fupd_wp. iApply ("Hrel" $! 0 []).
+    iApply fupd_wp. iApply ("Hrel" $! (RefId 0 [])).
     iSplitR.
     + iExists _. by iFrame.
     + rewrite tpool_mapsto_eq /tpool_mapsto_def.
@@ -49,6 +49,7 @@ Proof.
     rewrite HA.
     iDestruct "Hinterp" as %Hinterp.
     iInv specN as (tp σ') ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
+    iDestruct "Hj" as "[#Hs Hj]".
     rewrite tpool_mapsto_eq /tpool_mapsto_def /=.
     iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.
     move: Hvalid=> /auth_both_valid_discrete
diff --git a/theories/logic/model.v b/theories/logic/model.v
index fa24ce78752a005eae6fb8f818bc3a17b258dd98..18e244aa3ee093a294229eab9d8b229238a18bf1 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -26,8 +26,8 @@ Existing Instance lrel_persistent.
 Section lrel_ofe.
   Context `{Σ : gFunctors}.
 
-  Instance lrel_equiv : Equiv (lrel Σ) := λ A B, ∀ w1 w2, A w1 w2 ≡ B w1 w2.
-  Instance lrel_dist : Dist (lrel Σ) := λ n A B, ∀ w1 w2, A w1 w2 ≡{n}≡ B w1 w2.
+  Global Instance lrel_equiv : Equiv (lrel Σ) := λ A B, ∀ w1 w2, A w1 w2 ≡ B w1 w2.
+  Global Instance lrel_dist : Dist (lrel Σ) := λ n A B, ∀ w1 w2, A w1 w2 ≡{n}≡ B w1 w2.
   Lemma lrel_ofe_mixin : OfeMixin (lrel Σ).
   Proof. by apply (iso_ofe_mixin (lrel_car : lrel Σ → (val -d> val -d> iPropO Σ))). Qed.
   Canonical Structure lrelC := Ofe (lrel Σ) lrel_ofe_mixin.
@@ -53,9 +53,12 @@ End lrel_ofe.
 
 Arguments lrelC : clear implicits.
 
+Set Primitive Projections.
 Record ref_id := RefId {
   tp_id : nat;
   tp_ctx : list ectx_item }.
+Unset Primitive Projections.
+Add Printing Constructor ref_id.
 
 Canonical Structure ectx_itemO := leibnizO ectx_item.
 Canonical Structure ref_idO := leibnizO ref_id.
@@ -81,12 +84,12 @@ Section semtypes.
 
   Definition refines_def (E : coPset)
            (e : expr) (e'k : rhs_t) (A : lrel Σ) : iProp Σ :=
-    (∀ j K,
+    (∀ j : ref_id,
         match e'k with
-        | inl e' => refines_right (RefId j K) e'
-        | inr k  => ⌜j = tp_id k⌝ ∗ ⌜K = tp_ctx k⌝
+        | inl e' => refines_right j e'
+        | inr k  => ⌜j = k⌝
         end -∗
-        |={E,⊤}=> WP e {{ v, ∃ v', j ⤇ fill K (of_val v') ∗ A v v' }})%I.
+        |={E,⊤}=> WP e {{ v, ∃ v', refines_right j (of_val v') ∗ A v v' }})%I.
 
   Definition refines_aux : seal refines_def. Proof. by eexists. Qed.
   Definition refines := unseal refines_aux.
@@ -122,7 +125,7 @@ Section semtypes.
 
   Definition lrel_rec1 (C : lrelC Σ -n> lrelC Σ) (rec : lrel Σ) : lrel Σ :=
     LRel (λ w1 w2, ▷ C rec w1 w2)%I.
-  Instance lrel_rec1_contractive C : Contractive (lrel_rec1 C).
+  Global Instance lrel_rec1_contractive C : Contractive (lrel_rec1 C).
   Proof.
     intros n. intros P Q HPQ.
     unfold lrel_rec1. intros w1 w2. rewrite {1 4}/lrel_car /=.
@@ -259,7 +262,7 @@ Section related_facts.
   Proof.
     iIntros "H".
     rewrite refines_eq /refines_def.
-    iIntros (j K) "He'". pose (k := RefId j K).
+    iIntros (k) "He'".
     iSpecialize ("H" $! k with "He'").
     by iApply "H".
   Qed.
@@ -271,7 +274,7 @@ Section related_facts.
   Proof.
     iIntros "H1 H2".
     rewrite refines_eq /refines_def.
-    iIntros (j K) "[% %]".
+    iIntros (j) "%".
     iApply "H1". by destruct k; simplify_eq/=.
   Qed.
 
@@ -280,7 +283,7 @@ Section related_facts.
     (|={E1, E2}=> refines E2 e t A) -∗ refines E1 e t A.
   Proof.
     rewrite refines_eq /refines_def.
-    iIntros "H". iIntros (j K) "Hr /=".
+    iIntros "H". iIntros (j) "Hr /=".
     iMod "H" as "H". iApply ("H" with "Hr").
   Qed.
 
@@ -289,13 +292,13 @@ Section related_facts.
   Proof.
     rewrite refines_eq /refines_def.
     iIntros "H". simpl.
-    iSpecialize ("H" $! (tp_id k) (tp_ctx k) with "[%//]").
+    iSpecialize ("H" $! k with "[%//]").
     iMod "H" as "H". iModIntro.
-    iIntros (j K) "[-> ->]". done.
+    iIntros (j) "->". done.
   Qed.
 
   Global Instance elim_fupd_refines p E1 E2 e t P A :
-   (* TODO: DF: look at the booleans here *)
+   (* DF: look at the booleans here *)
    ElimModal True p false (|={E1,E2}=> P) P
      (refines E1 e t A) (refines E2 e t A).
   Proof.
@@ -334,14 +337,15 @@ Section monadic.
   Proof.
     iIntros "Hm Hf".
     rewrite refines_eq /refines_def /refines_right.
-    iIntros (j K₁) "[#Hs Hj] /=".
+    iIntros (j) "[#Hs Hj] /=".
     rewrite -fill_app.
-    iMod ("Hm" with "[$Hs $Hj]") as "Hm".
+    iMod ("Hm" $! (RefId (tp_id j) (K' ++ tp_ctx j)) 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/=".
+    iSpecialize ("Hf" with "HA").
+    iMod ("Hf" $! j with "Hj") as "$".
   Qed.
 
   Lemma refines_ret E e1 e2 v1 v2 (A : lrel Σ) :
@@ -352,7 +356,7 @@ Section monadic.
     rewrite /IntoVal.
     iIntros (<-<-) "HA".
     rewrite refines_eq /refines_def.
-    iIntros (j K) "[#Hs Hj] /=".
+    iIntros (j) "Hj /=".
     iMod "HA" as "HA". iModIntro.
     iApply wp_value. iExists _. by iFrame.
   Qed.
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index 6e290564d016473c4888872eeb028e99016e085a..7f9ab5aab6a3827939e06ef6e50a6d9889ae85a8 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -30,7 +30,7 @@ Section rules.
   Proof.
     intros Hpure HÏ•.
     rewrite refines_eq /refines_def.
-    iIntros "IH" ; iIntros (j K) "Hs /=".
+    iIntros "IH" ; iIntros (j) "Hs".
     iModIntro. wp_pures.
     iApply fupd_wp. iApply ("IH" with "Hs").
   Qed.
@@ -44,7 +44,7 @@ Section rules.
   Proof.
     intros Hpure HÏ•.
     rewrite refines_eq /refines_def.
-    iIntros "IH" ; iIntros (j K) "Hs /=".
+    iIntros "IH" ; iIntros (j) "Hs /=".
     iMod ("IH" with "Hs") as "IH".
     iModIntro. by wp_pures.
   Qed.
@@ -56,7 +56,7 @@ Section rules.
   Proof.
     rewrite refines_eq /refines_def.
     iIntros "He".
-    iIntros (j K') "Hs /=".
+    iIntros (j) "Hs /=".
     iModIntro. iApply wp_bind.
     iApply (wp_wand with "He").
     iIntros (v) "Hv".
@@ -71,7 +71,7 @@ Section rules.
   Proof.
     rewrite refines_eq /refines_def.
     iIntros "Hlog".
-    iIntros (j K') "Hs /=". iModIntro.
+    iIntros (j) "Hs /=". iModIntro.
     iApply wp_bind. iApply wp_atomic; auto.
     iMod "Hlog" as "He". iModIntro.
     iApply (wp_wand with "He").
@@ -89,9 +89,9 @@ Section rules.
     ⊢ REL t << fill K' e @ E : A.
   Proof.
     rewrite refines_eq /refines_def => Hpure HÏ•.
-    iIntros "Hlog". iIntros (j K) "Hs /=".
-    tp_pures ({| tp_id := j; tp_ctx := K |}) ; auto.
-    iApply ("Hlog" with "Hs").
+    iIntros "Hlog". iIntros (j) "Hj /=".
+    tp_pures j ; auto.
+    iApply ("Hlog" with "Hj").
   Qed.
 
   Lemma refines_right_bind k K e :
@@ -110,7 +110,7 @@ Section rules.
   Proof.
     rewrite refines_eq /refines_def.
     iIntros "He".
-    iIntros (j K) "Hs /=".
+    iIntros (j) "Hs /=".
     rewrite refines_right_bind /=.
     iMod ("He" with "Hs") as (v) "[Hs He]".
     rewrite -refines_right_bind'.
@@ -251,14 +251,14 @@ Section rules.
   Proof.
     rewrite refines_eq /refines_def.
     iIntros "H".
-    iIntros (j K) "Hs /=".
-    tp_fork ({| tp_id := j; tp_ctx := K |}) as k' "Hk'". iModIntro.
+    iIntros (j) "Hs /=".
+    tp_fork j 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 _. rewrite /refines_right.
-      iDestruct "Hs" as "[_ $]". done.
+      eauto with iFrame.
   Qed.
 
   (** This rule is useful for proving that functions refine each other *)