diff --git a/coq-reloc.opam b/coq-reloc.opam
index ebbeaf714b2ef2b2a2adcb84fdf13a29eba5b77d..f1cbb1d4a07efa70ccee39d51a84105f0b4a7c88 100644
--- a/coq-reloc.opam
+++ b/coq-reloc.opam
@@ -6,7 +6,7 @@ bug-reports: "https://gitlab.mpi-sws.org/dfrumin/reloc/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/dfrumin/reloc.git"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2024-02-02.1.b30c53e2") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2024-02-16.1.06f499e0") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
 
diff --git a/theories/examples/coinflip.v b/theories/examples/coinflip.v
index 3da79c5284a167d82290b092ba6da4aed40afe27..e1e2f27af7696efa6efde4e72040aaf4576e9f46 100644
--- a/theories/examples/coinflip.v
+++ b/theories/examples/coinflip.v
@@ -103,13 +103,11 @@ Section proofs.
         rel_store_l; repeat rel_pure_l.
       + rel_apply_r (refines_rand_r (extract_bool vs)).
         rel_store_r.
-        rel_apply_l (refines_release_l with "Hlk Hlocked [-]").
-        { iExists vs. iFrame. iLeft. iFrame. }
+        rel_apply_l (refines_release_l with "Hlk Hlocked [$]").
         iNext. rel_values.
       + rel_apply_r (refines_rand_r (extract_bool vs)).
         rel_store_r.
-        rel_apply_l (refines_release_l with "Hlk Hlocked [-]").
-        { iExists vs. iFrame. iLeft. iFrame. }
+        rel_apply_l (refines_release_l with "Hlk Hlocked [$]").
         iNext. rel_values.
   Qed.
 
@@ -130,13 +128,12 @@ Section proofs.
            (∃ (b : bool), is_locked_r lk false
                         ∗ ce ↦ #b
                         ∗ (cl ↦ₛ NONEV ∨ cl ↦ₛ SOMEV #b))%I
-            with "[-]") as "#Hinv".
-    { iNext. iExists false. iFrame. }
+            with "[$]") as "#Hinv".
     iApply refines_pair.
     - rel_pure_l; rel_pure_r. iApply refines_arrow. iIntros (??) "!> _".
       rel_pure_l; rel_rec_l; rel_pure_r; rel_rec_r. repeat rel_pure_l.
       rel_load_l_atomic. iInv coinN as (b) "(Hlk & Hce & H)" "Hclose".
-      iModIntro. iExists _. iFrame. iNext. iIntros "Hce". repeat rel_pure_r.
+      iModIntro. iFrame. iNext. iIntros "Hce". repeat rel_pure_r.
       rel_apply_r (refines_acquire_r with "Hlk"). iIntros "Hlk".
       repeat rel_pure_r.
       iDestruct "H" as "[Hcl|Hcl]"; rel_load_r; repeat rel_pure_r.
@@ -144,28 +141,24 @@ Section proofs.
         rel_store_r. repeat rel_pure_r.
         rel_resolveproph_r. repeat rel_pure_r.
         rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
-        repeat rel_pure_r. iMod ("Hclose" with "[-]") as "_".
-        { eauto with iFrame. }
+        repeat rel_pure_r. iMod ("Hclose" with "[$]") as "_".
         rel_values.
       + rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
-        repeat rel_pure_r. iMod ("Hclose" with "[-]") as "_".
-        { eauto with iFrame. }
+        repeat rel_pure_r. iMod ("Hclose" with "[$]") as "_".
         rel_values.
     - rel_pure_l; rel_pure_r. iApply refines_arrow. iIntros (??) "!> _".
       rel_pure_l; rel_rec_l; rel_pure_r; rel_rec_r. repeat rel_pure_l.
       rel_apply_l refines_rand_l. iNext. iIntros (b).
       rel_store_l_atomic. iInv coinN as (b') "(Hlk & Hce & H)" "Hclose".
-      iModIntro. iExists _. iFrame. iNext. iIntros "Hce". repeat rel_pure_r.
+      iModIntro. iFrame. iNext. iIntros "Hce". repeat rel_pure_r.
       rel_apply_r (refines_acquire_r with "Hlk"). iIntros "Hlk".
       repeat rel_pure_r.
       iDestruct "H" as "[Hcl|Hcl]"; rel_store_r; repeat rel_pure_r.
       + rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
-        repeat rel_pure_r. iMod ("Hclose" with "[-]") as "_".
-        { eauto with iFrame. }
+        repeat rel_pure_r. iMod ("Hclose" with "[$]") as "_".
         rel_values.
       + rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
-        repeat rel_pure_r. iMod ("Hclose" with "[-]") as "_".
-        { eauto with iFrame. }
+        repeat rel_pure_r. iMod ("Hclose" with "[$]") as "_".
         rel_values.
   Qed.
 
@@ -205,11 +198,11 @@ Section proofs.
         rel_apply_r (refines_rand_r b). repeat rel_pure_r.
         rel_cmpxchg_suc_r. repeat rel_pure_r.
         rel_apply_l (refines_release_l with "Hlk Hlocked [-]").
-        { iExists vs'. iFrame. iRight. iExists b. iFrame. }
+        { iExists vs'. iFrame. iRight. iFrame. }
         iNext. repeat rel_pure_l; rel_values.
       + repeat rel_pure_r.
         rel_apply_l (refines_release_l with "Hlk Hlocked [-]").
-        { iExists vs. iFrame. iRight. iExists x. iFrame. }
+        { iExists vs. iFrame. iRight. iFrame. }
         iNext. repeat rel_pure_l; rel_values.
     - rel_pure_l; rel_pure_r. iApply refines_arrow. iIntros (??) "!> _".
       rel_pure_l; rel_rec_l; rel_pure_r; rel_rec_r. repeat rel_pure_l.
@@ -244,7 +237,7 @@ Section proofs.
           ∗ (c' ↦ₛ NONEV ∗ c ↦ NONEV
             ∨ ∃ (b : bool), c' ↦ₛ SOMEV #b ∗ c ↦ SOMEV #b))%I
             with "[-]") as "#Hinv".
-    { iNext. iFrame. iRight. iExists false. iFrame. }
+    { iNext. iFrame. iRight. iFrame. }
     do 2 rel_pure_r.
 
     iApply refines_pair.
@@ -275,7 +268,7 @@ Section proofs.
           { eauto with iFrame. }
           rel_values.
         * iDestruct "H" as (x) "[Hc' Hc]".
-          iModIntro; iExists _. iFrame. iSplit; last first.
+          iModIntro; iFrame. iSplit; last first.
           { iIntros (?); simplify_eq/=. }
           iIntros (_). iNext. iIntros "Hc".
           rel_pures_l.
@@ -283,7 +276,7 @@ Section proofs.
           { eauto with iFrame. }
           iApply "IH".
       + iClear "IH".
-        iDestruct "H" as (b) "[Hc' Hc]". iExists _. iFrame. iNext. iIntros "Hc".
+        iDestruct "H" as (b) "[Hc' Hc]". iFrame. iNext. iIntros "Hc".
         repeat rel_pure_l.
         rel_apply_r (refines_acquire_r with "Hlk").
         iIntros "Hlk". repeat rel_pure_r. rel_load_r.
@@ -297,7 +290,7 @@ Section proofs.
       repeat rel_rec_l. repeat rel_rec_r. repeat rel_pure_l. repeat rel_pure_r.
       rel_store_l_atomic. iInv coinN as "(Hlk & [[Hc' Hc]|H])" "Hclose";
         iModIntro.
-      + iExists _. iFrame. iNext. iIntros "Hc".
+      + iFrame. iNext. iIntros "Hc".
         rel_apply_r (refines_acquire_r with "Hlk").
         iIntros "Hlk". repeat rel_pure_r. rel_store_r.
         repeat rel_pure_r. rel_apply_r (refines_release_r with "Hlk").
@@ -306,7 +299,7 @@ Section proofs.
         { eauto with iFrame. }
         rel_values.
       + iDestruct "H" as (x) "[Hc' Hc]".
-        iExists _. iFrame. iNext. iIntros "Hc".
+        iFrame. iNext. iIntros "Hc".
         rel_apply_r (refines_acquire_r with "Hlk").
         iIntros "Hlk". repeat rel_pure_r. rel_store_r.
         repeat rel_pure_r. rel_apply_r (refines_release_r with "Hlk").
diff --git a/theories/examples/folly_queue/refinement.v b/theories/examples/folly_queue/refinement.v
index 85425e40b2843fd972ff7d4d2f3e73428c93d8b1..1f0315848abb6d53fa7600ff9e7cfa181d599d0c 100644
--- a/theories/examples/folly_queue/refinement.v
+++ b/theories/examples/folly_queue/refinement.v
@@ -723,7 +723,6 @@ Section queue_refinement.
         iFrame. iFrame "HA".
         rewrite big_sepL2_nil.
         iSplitL; last done.
-        iExists popTicket, (pushTicket + 1), _, _, _.
         assert ((pushTicket + 1)%Z = (pushTicket + 1)%nat) as -> by lia.
         assert (popTicket `max` (pushTicket + 1) = pushTicket + 1) as -> by lia.
         assert (popTicket - (pushTicket + 1) = 0) as -> by lia.
@@ -845,8 +844,6 @@ Section queue_refinement.
 
       iMod ("Hcl" with "[-arrPts Hturn Htok]") as "_".
       { iNext. iExists [], []. simpl. iFrame.
-        iExists (popTicket + 1), pushTicket, _, _, _.
-        simpl.
         assert ((popTicket + 1)%Z = (popTicket + 1)%nat) as ->; first lia.
         replace ((popTicket + 1) `max` pushTicket) with (popTicket + 1) by lia.
         (* assert (popTicket `max` pushTicket + 1 = (popTicket + 1) `max` pushTicket) as ->; first lia. *)
@@ -903,8 +900,9 @@ Section queue_refinement.
         iCombine "Hi Hpush" as "Hpush".
         rewrite -big_sepS_insert; last set_solver by lia.
         (* rewrite difference_union_distr_l_L. *)
-        replace ({[popTicket]} ∪ set_seq 0 pushTicket ∖ {[popTicket]}) with (set_seq (C:=gset nat) 0 pushTicket) by set_solver by lia.
-        iExists _, _, _, _, _. by iFrame. }
+        replace ({[popTicket]} ∪ set_seq 0 pushTicket ∖ {[popTicket]})
+          with (set_seq (C:=gset nat) 0 pushTicket) by set_solver by lia.
+        by iFrame. }
 
       iModIntro. iNext. iModIntro.
       iDestruct (map_list_agree with "Hag Hag'") as %->.
@@ -936,7 +934,6 @@ Section queue_refinement.
       (* Close the invariant. *)
       iMod ("Hcl" with "[-arrPts Hturn]") as "_".
       { iNext. iExists xs, xsâ‚›'. iFrame.
-        iExists (popTicket + 1), pushTicket, _, _, _.
         assert ((popTicket + 1)%Z = (popTicket + 1)%nat) as -> by lia.
         assert (popTicket + 1 - pushTicket = 0) as -> by lia.
         iFrame.
@@ -1005,7 +1002,7 @@ Section queue_refinement.
     iMod (own_alloc (set_above 0)) as (γt) "Htok"; first done.
     iMod (own_alloc (● ∅ : requestRegR)) as (γm) "Hdec"; first by apply auth_auth_valid.
     iMod (inv_alloc queueN _ (I A γt γm γl q ℓpop ℓpush ℓarr SEQs _ _) with "[-]") as "#Hinv".
-    { iNext. iExists [], []. simpl. iFrame. iExists 0, 0, ∅, 1%Qp, ∅. cbn. iFrame.
+    { iNext. iExists [], []. simpl. iFrame.
       rewrite !dom_empty_L !big_sepS_empty. iFrame. done. }
 
     iApply refines_pair.
diff --git a/theories/examples/folly_queue/turnSequencer.v b/theories/examples/folly_queue/turnSequencer.v
index 1cff42b6285f7855c2c3cd4d2da33b90fff2439a..2df2168b7a18c5cc0bf9c2bc5c640c91b449868a 100644
--- a/theories/examples/folly_queue/turnSequencer.v
+++ b/theories/examples/folly_queue/turnSequencer.v
@@ -146,7 +146,7 @@ Section spec.
     iDestruct "â„“Pts" as "[â„“Pts â„“Pts']".
     iDestruct (turns_add with "Hturns Ht") as "Hturns".
     iMod ("Hcl" with "[-HÏ•]") as "_".
-    { iNext. iExists (n + 1). iFrame. iLeft. iFrame. iExists _; eauto with iFrame. }
+    { iNext. iExists (n + 1). eauto with iFrame. }
     iModIntro. by iApply "HÏ•".
   Qed.
 
diff --git a/theories/examples/red_blue_flag.v b/theories/examples/red_blue_flag.v
index f38f314bf56e6ede8dbef8c74cf1c9a3cd3d3e02..a4f9f8bcdf74e0b04aeb7901f2c92aa66c3c3fd0 100644
--- a/theories/examples/red_blue_flag.v
+++ b/theories/examples/red_blue_flag.v
@@ -238,7 +238,7 @@ Section proofs.
     iMod no_offer_alloc as (γ) "Hno".
     iMod (own_alloc (1%Qp)) as (γ') "Htok"; first done.
     iMod (inv_alloc iN _ (I γ γ' rf bf chan lk) with "[-]") as "#Hinv".
-    { iNext. iFrame. iExists _. iFrame. iExists 0. iFrame. iLeft. iFrame. done. }
+    { iNext. iFrame. iExists 0. iFrame. iLeft. iFrame. done. }
     iApply refines_pair.
 
     (* Refines read. *)
@@ -299,17 +299,17 @@ Section proofs.
 
         iDestruct ("Hrest" with "Hj") as "Hoff".
         iMod ("Hclose" with "[-]") as "_".
-        { iNext. iExists _. iFrame. rewrite /is_locked_r. iExists _. iFrame. done. }
+        { by iFrame. }
         rel_pures_l.
         rel_values. }
       iIntros "Hoff".
-      iMod ("Hclose" with "[-]") as "_". { iNext. iExists _. iFrame. }
+      iMod ("Hclose" with "[$]") as "_".
       rel_pures_l.
 
       (* The second CAS. *)
       rel_cmpxchg_l_atomic.
       iInv iN as (?) "(>Hlk & rfPts & bfPts & Hchan)" "Hclose".
-      iExists _. iFrame "rfPts". iModIntro. iSplit.
+      iFrame "rfPts". iModIntro. iSplit.
       2: {
         iIntros ([= ->]). iNext. iIntros "rfPts".
         rel_pures_l.
@@ -357,8 +357,7 @@ Section proofs.
            and use the IH. *)
         iIntros (Heq). simplify_eq/=.
         iNext. iIntros "Hchan".
-        iMod ("Hclose" with "[-IH Hk]") as "_".
-        { iNext. iExists _. iFrame. iExists _. iFrame. }
+        iMod ("Hclose" with "[$]") as "_".
         iApply (refines_combine with "[] Hk").
         do 2 rel_pure_l _.
         iApply "IH". }
@@ -404,7 +403,7 @@ Section proofs.
       iDestruct (offer_combine with "Hoff Hoff'") as "(<- & Hoff)".
       iDestruct (offer_token_split with "Htok") as "[Htok Htok']".
       iMod ("Hclose" with "[-IH Hj Hoff Htok]") as "_".
-      { iNext. iExists _. iFrame. iExists n. iFrame. iRight.
+      { iNext. iExists _. iFrame. iRight.
         iExists k. iRight. by iFrame. }
       rel_pures_l.
 
diff --git a/theories/examples/stack/refinement.v b/theories/examples/stack/refinement.v
index e98b244233c1be962082d827ba8de113f9e77b7f..25071c1535a52dcdef9a5d1ad725eb4341bbd9fa 100644
--- a/theories/examples/stack/refinement.v
+++ b/theories/examples/stack/refinement.v
@@ -81,9 +81,8 @@ Section proof.
       rel_apply_r (refines_CG_push_r with "Hls2").
       iIntros "Hls2".
       iMod ("Hclose" with "[-]").
-      { iNext. rewrite {2}/sinv. iExists _. iFrame.
-        iExists (v::ls1),_. simpl. iFrame "Hls2 Hvv HA".
-        iExists _. iFrame. }
+      { iNext. rewrite {2}/sinv. iFrame.
+        iExists (v::ls1). simpl. auto with iFrame. }
       rel_pures_l. rel_values.
   Qed.
 
@@ -108,13 +107,13 @@ Section proof.
       rel_apply_r (refines_CG_pop_fail_r with "Hls2").
       iIntros "Hls2". simpl in *.
       iMod ("Hclose" with "[Hstk Hls2]") as "_".
-      { iExists _. iFrame. iExists [], []. iFrame; auto. }
+      { iExists _. iFrame. iExists []. iFrame; auto. }
       rel_load_l.
       rel_pures_l. rel_values.
       iModIntro. iExists _,_. eauto.
     - iDestruct "Hls1" as (z1) "[Hls1 Hrest]".
       iMod ("Hclose" with "[Hstk Hls2]") as "_".
-      { iExists _. iFrame. iExists (h1 :: ls1), _. simpl. auto. }
+      { iExists _. iFrame. iExists (h1 :: ls1). simpl. auto. }
       rel_load_l. rel_pures_l.
       rel_cmpxchg_l_atomic.
       iInv N as (istk') "(>Hstk & Hlnk)" "Hclose".
@@ -134,7 +133,7 @@ Section proof.
         rel_apply_r (refines_CG_pop_suc_r with "Hst").
         iIntros "Hst".
         iMod ("Hclose" with "[-]") as "_".
-        { iExists _. iFrame. iExists _, _; auto. }
+        { iExists _. iFrame. iExists _; auto. }
         rel_values. iModIntro. iExists _,_; eauto.
   Qed.
 
@@ -162,8 +161,7 @@ Section proof.
         as "#Hinv".
       { iNext. iExists _. iFrame. iExists [],[]. simpl.
         iSplitL "Hisk"; first by eauto.
-        rewrite right_id. rewrite /is_stack.
-        iExists _,_; eauto with iFrame. }
+        rewrite right_id. rewrite /is_stack. eauto with iFrame. }
       iModIntro. iExists _. eauto with iFrame.
     - rel_pure_l. rel_pure_r. iApply refines_arrow_val.
       iModIntro. iIntros (st1 st2) "Hst".
diff --git a/theories/examples/stack_helping/helping_wrapper.v b/theories/examples/stack_helping/helping_wrapper.v
index ac20b43e873b74ed6882824e7c3ac004b86cfa59..7684d7d40838464060f30fb8b40ce3366d4707e3 100644
--- a/theories/examples/stack_helping/helping_wrapper.v
+++ b/theories/examples/stack_helping/helping_wrapper.v
@@ -410,8 +410,7 @@ Section stack_example.
       rel_apply_r (refines_CG_pop_suc_r with "[Hst2 Hl]").
       { iExists st2l,#lk'. rewrite /is_locked_r. by eauto with iFrame. }
       iIntros "Hst2".
-      iMod ("Hcl" with "[-Hcont Hj]") as "_".
-      { iNext. iExists _,_. by eauto with iFrame. }
+      iMod ("Hcl" with "[$]") as "_".
       by iApply "Hcont". }
   { rel_arrow_val. iIntros (??) "[-> ->]". rel_pures_l. rel_pures_r.
     iDestruct "Hstack" as (st1l lk1 ->) "[#HstI #Hstack]". rewrite /stackI.
@@ -432,8 +431,7 @@ Section stack_example.
       rel_rec_r. rel_pures_r.
       rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
       iMod ("Hcl" with "[-Hl1 Hlocked]") as "_".
-      { iNext. iExists [], []. simpl. iFrame.
-        rewrite right_id. iExists _,_. eauto with iFrame. }
+      { iNext. iExists [], []. simpl. by iFrame. }
       rel_apply_l (refines_release_l with "HstI Hlocked [Hl1]").
       { iExists []. eauto with iFrame. }
       iNext. rel_pures_l; rel_pures_r; rel_values.
@@ -452,8 +450,7 @@ Section stack_example.
       rel_apply_r (refines_release_r with "Hlk"). iIntros "Hlk".
       iDestruct "Hl1" as "[Hl1 Hst1]".
       iMod ("Hcl" with "[-Hl1 Hlocked]") as "_".
-      { iNext. iExists _,_. simpl. iFrame.
-        iExists _,_. eauto with iFrame. }
+      { by iFrame. }
       rel_pures_l.
       rel_apply_l (refines_release_l with "HstI Hlocked [Hl1]").
       { iExists _. eauto with iFrame. }
@@ -524,8 +521,7 @@ Section stack_example.
                       (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.
-      iExists _,_. eauto with iFrame. }
+    { iNext. iExists [], []; simpl; by iFrame. }
     iMod (inv_alloc iN _ (I A γo mb _) with "[-Hlk1]") as "#Hofferinv".
     { iNext. iExists ∅. iFrame. iApply offerInv_empty. }
     iApply refines_pair.
diff --git a/theories/examples/stack_helping/stack.v b/theories/examples/stack_helping/stack.v
index 2bbfab190a50ff88a6974e56047ab2920e235162..38b197177f1615a7d511e6e38e2238795f04620e 100644
--- a/theories/examples/stack_helping/stack.v
+++ b/theories/examples/stack_helping/stack.v
@@ -557,9 +557,7 @@ Section refinement.
     iMod (inv_alloc stackN _ (stackInv A γo st mb (#st', lk)%V) with "[-]") as "#Hinv".
     { iNext. unfold stackInv.
       iExists None, _, [],[]. iFrame.
-      iSplit; eauto.
-      - rewrite /is_stack. iExists _,_. eauto with iFrame.
-      - iSplit; first done. iApply offerInv_empty. }
+      iSplit; eauto. iSplit; first done. iApply offerInv_empty. }
     iApply refines_pair; last first.
     (* * Push refinement *)
     { rel_arrow_val. iIntros (h1 h2) "#Hh"; simplify_eq/=.
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index c81377b0a6b9175f2c7ae3a62f3aeba0b42422dc..e2760a9d6a1643893a724c04508c67eb545adce1 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -173,8 +173,6 @@ Section refinement.
     iPoseProof "H" as "H2".
     iMod "H" as (o n) "(Hlo & Hln & Hissued & HR & Hrest)". iModIntro.
     iExists _; iFrame.
-    iSplitL "Hlo HR".
-    { iExists _. iFrame. }
     iSplit.
     - iDestruct "Hrest" as "[H _]".
       iIntros "[Hln Ho]".
@@ -200,11 +198,9 @@ Section refinement.
       case_decide; simplify_eq/=; rel_if_l.
       (* Whether the ticket is called out *)
       + iDestruct "Hrest" as "[_ H]".
-        iApply ("H" with "[-HP] HP").
-        { iExists _. iFrame. }
+        iApply ("H" with "[$] HP").
       + iDestruct "Hrest" as "[H _]".
-        iMod ("H" with "[-HP Hm]") as "_".
-        { iExists _. iFrame. }
+        iMod ("H" with "[$]") as "_".
         iApply ("IH" with "HP Hm").
   Qed.
 
@@ -221,8 +217,6 @@ Section refinement.
     iModIntro.
     openI.
     iModIntro. iExists _,_; iFrame.
-    iSplitL "Hbticket Hl'".
-    { iExists _. iFrame. }
     clear st o n.
     iSplit.
     - iIntros (o). iDestruct 1 as (n) "(Hlo & Hln & Hissued & Hrest)".
@@ -235,8 +229,7 @@ Section refinement.
       { iDestruct (ticket_nondup with "Ht Ht'") as %[]. }
       rel_apply_r (refines_acquire_r with "Hl'").
       iIntros "Hl'".
-      iMod ("Hcl" with "[-]") as "_".
-      { iNext. iExists _,_,_; by iFrame. }
+      iMod ("Hcl" with "[$]") as "_".
       rel_values.
   Qed.