diff --git a/theories/examples/stack/CG_stack.v b/theories/examples/stack/CG_stack.v
index 250a1f28eb2672a60b6e60f0777b045679b6b4eb..9bfb5ac02254dcaf49dcaddbdbd2860107d20d9b 100644
--- a/theories/examples/stack/CG_stack.v
+++ b/theories/examples/stack/CG_stack.v
@@ -28,7 +28,9 @@ Definition CG_locked_pop : val := λ: "stt",
   release (Snd "stt");; "v".
 
 Definition CG_new_stack : val := λ: <>,
-  (ref NIL, newlock #())%E.
+  let: "st" := ref NIL in
+  let: "lk" := newlock #() in
+  ("st", "lk")%E.
 
 Definition CG_stack : val := Λ:
   (CG_new_stack, λ: "stt", CG_locked_pop "stt",
@@ -40,6 +42,11 @@ Fixpoint val_of_list (ls : list val) : val :=
   | v::vs => CONSV v (val_of_list vs)
   end.
 
+Instance val_to_list_inj : Inj (=@{list val}) (=@{val}) val_of_list.
+Proof.
+  intros ls1. induction ls1 as [|h1 ls1]=>ls2; destruct ls2; naive_solver.
+Qed.
+
 Definition is_stack `{!relocG Σ} (rs : val) (ls : list val) : iProp Σ :=
   ∃ (st : loc) l, ⌜rs = (#st, l)%V⌝ ∗ is_locked_r l false ∗ st ↦ₛ val_of_list ls.
 
diff --git a/theories/examples/stack/refinement.v b/theories/examples/stack/refinement.v
index cf961ac345ad0ca2ca3cd2875c154472627018ac..a26b59641f23f2cfc466cf6d4d4057a35813c2c9 100644
--- a/theories/examples/stack/refinement.v
+++ b/theories/examples/stack/refinement.v
@@ -176,8 +176,8 @@ Section proof.
       iIntros (??) "_". repeat rel_pure_l. repeat rel_pure_r.
       rel_alloc_l istk as "Hisk".
       rel_alloc_l st as "Hst".
-      rel_apply_r refines_newlock_r. iIntros (l) "Hl".
-      rel_pure_r. rel_alloc_r st' as "Hst'". rel_pure_r.
+      rel_alloc_r st' as "Hst'". rel_pures_r.
+      rel_apply_r refines_newlock_r. iIntros (l) "Hl". rel_pures_r.
       rel_values.
       iMod (inv_alloc (stackN.@(st,(#st', l)%V)) _ (sinv A st (#st', l)%V) with "[-]")
         as "#Hinv".
diff --git a/theories/examples/various.v b/theories/examples/various.v
index 146fdeef4127b1c61b141e4e07ea6e20df570d7c..26dc81dec33d731e5b8a7098b2d1a6f6d288398c 100644
--- a/theories/examples/various.v
+++ b/theories/examples/various.v
@@ -293,7 +293,7 @@ Section proofs.
     iApply refines_arrow; auto.
     iIntros "!#" (f1 f2) "#Hf".
     rel_let_l. rel_let_r.
-    rel_apply_l (refines_acquire_l N _ l with "Hl").
+    rel_apply_l (refines_acquire_l N _ #l with "Hl").
     iNext. iIntros "Hlocked". iDestruct 1 as (n m) "[Hx Hy]".
     repeat rel_pure_l. rel_store_l. repeat rel_pure_l.
     iApply (refines_seq () with "[Hf]").
@@ -306,7 +306,7 @@ Section proofs.
       rel_values. }
     rel_load_l. repeat rel_pure_l.
     rel_load_r. repeat rel_pure_r.
-    rel_apply_l (refines_release_l N _ l γ with "Hl Hlocked [Hx Hy]"); eauto.
+    rel_apply_l (refines_release_l N _ #l γ with "Hl Hlocked [Hx Hy]"); eauto.
     { iExists _,_. iFrame. }
     iNext. repeat rel_pure_l.
     rel_values.
diff --git a/theories/experimental/helping/helping_stack.v b/theories/experimental/helping/helping_stack.v
index bd191d09efb5558b02de77f5c35437dbfe4fc5c5..be39de80d5ada418fd3877b1b33a09551e9c6aef 100644
--- a/theories/experimental/helping/helping_stack.v
+++ b/theories/experimental/helping/helping_stack.v
@@ -573,9 +573,8 @@ Section refinement.
     rel_values. iModIntro. iIntros (A). iModIntro.
     iIntros (? ?) "[-> ->]".
     rel_rec_r. rel_pures_r. rel_rec_r.
+    rel_alloc_r st' as "Hst'". rel_pures_r.
     rel_apply_r refines_newlock_r. iIntros (lk) "Hlk".
-    rel_pures_r.
-    rel_alloc_r st' as "Hst'".
     rel_pure_r. rel_pure_r.  rel_pure_r.  rel_pure_r.  rel_pure_r.
     rel_rec_l. rel_pures_l.
     rel_alloc_l mb as "Hmb". rel_pures_l.
diff --git a/theories/lib/lock.v b/theories/lib/lock.v
index f44599138b265266fb47deb28e15bde6fefd97ea..6cbe7c8a15ce6adaac04b2fff26e80b876f002e1 100644
--- a/theories/lib/lock.v
+++ b/theories/lib/lock.v
@@ -60,12 +60,12 @@ Section lockG_rules.
     iApply "Hlog". iExists l. eauto.
   Qed.
 
-  Lemma refines_release_l (R : iProp Σ) (lk : loc) γ K t A :
-    is_lock γ #lk R -∗
+  Lemma refines_release_l (R : iProp Σ) (lk : val) γ K t A :
+    is_lock γ lk R -∗
     locked γ -∗
     R -∗
     ▷(REL fill K (#() : expr) << t : A) -∗
-    REL fill K (release #lk) << t: A.
+    REL fill K (release lk) << t: A.
   Proof.
     iIntros "Hlock Hlocked HR Hlog".
     iDestruct "Hlock" as (l) "[% #?]"; simplify_eq.
@@ -78,10 +78,10 @@ Section lockG_rules.
     iApply "Hlog".
   Qed.
 
-  Lemma refines_acquire_l (R : iProp Σ) (lk : loc) γ K t A :
-    is_lock γ #lk R -∗
+  Lemma refines_acquire_l (R : iProp Σ) (lk : val) γ K t A :
+    is_lock γ lk R -∗
     ▷(locked γ -∗ R -∗ REL fill K (of_val #()) << t: A) -∗
-    REL fill K (acquire #lk) << t: A.
+    REL fill K (acquire lk) << t: A.
   Proof.
     iIntros "#Hlock Hlog".
     iLöb as "IH".