diff --git a/coq-iris-examples.opam b/coq-iris-examples.opam
index 1d6a5157e88853664f96ba440371861f630b4a1e..b3c04ca92059da811971e3a2e546a6cb5062ff06 100644
--- a/coq-iris-examples.opam
+++ b/coq-iris-examples.opam
@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/examples.git"
 synopsis: "A collection of case studies for Iris -- not meant to be used as a dependency of anything"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2024-02-09.1.caaff570") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2024-02-16.1.06f499e0") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
 
diff --git a/theories/concurrent_stacks/concurrent_stack3.v b/theories/concurrent_stacks/concurrent_stack3.v
index 233bf783c7e1eb4102210044acdf8efc24003977..932a1f19f58b3b83e1e18fd1795d084b29b6d295 100644
--- a/theories/concurrent_stacks/concurrent_stack3.v
+++ b/theories/concurrent_stacks/concurrent_stack3.v
@@ -106,7 +106,7 @@ Section stack_works.
       iMod (pointsto_persist with "Hl'") as "#Hl'".
       iMod ("Hupd" with "HP") as "[HP HΨ]".
       iMod ("Hclose" with "[Hl HP Hlist]") as "_".
-      { iNext; iExists (Some _), (v :: xs); iFrame; iExists _; iFrame; auto. }
+      { iNext; iExists (Some _), (v :: xs); iFrame "#∗". }
       iModIntro.
       wp_pures.
       by iApply ("HΦ" with "HΨ").
diff --git a/theories/concurrent_stacks/concurrent_stack4.v b/theories/concurrent_stacks/concurrent_stack4.v
index 22224c11da5775a64ec0f9900c95b410b0a0986d..ea991680fcf17c9d0f9b76343a8c9b27b9152fc2 100644
--- a/theories/concurrent_stacks/concurrent_stack4.v
+++ b/theories/concurrent_stacks/concurrent_stack4.v
@@ -340,7 +340,7 @@ Section proofs.
         iMod ("Hupd" with "HP") as "[HP HΨ]".
         iMod "Hupd'" as "_".
         iMod ("Hclose" with "[Hl HP Hlist]") as "_".
-        { iNext; iExists (Some _), (v' :: xs); iFrame; iExists _; iFrame; auto. }
+        { iNext; iExists (Some _), (v' :: xs); iFrame "#∗". }
         iModIntro.
         wp_pures.
         by iApply ("HΦ" with "HΨ").
diff --git a/theories/hocap/concurrent_runners.v b/theories/hocap/concurrent_runners.v
index 0b9142ef0c483dbe601d1986eaf3d9d84b88d31b..cfe0063cae536946f62891795264927f9ac7ff20 100644
--- a/theories/hocap/concurrent_runners.v
+++ b/theories/hocap/concurrent_runners.v
@@ -228,7 +228,7 @@ Section contents.
     iMod (inv_alloc (N.@"task") _ (task_inv γ γ' status res (Q a))%I with "[-HP HΦ Htask Hinit]") as "#Hinv".
     { iNext. iLeft. iFrame. }
     wp_pures. iModIntro. iApply "HΦ".
-    iFrame. iSplitL; iExists _,_,_; iFrame "Hinv"; eauto.
+    iFrame "#∗". eauto.
   Qed.
 
   Lemma task_Join_spec γb γ γ' (r t a : val) P Q :
@@ -248,14 +248,14 @@ Section contents.
       iMod ("Hcl" with "[Hstate Hres]") as "_".
       { iNext; iLeft; iFrame. }
       iModIntro. wp_op. wp_if.
-      rewrite /task_Join. iApply ("IH" with "[$Htoken] HΦ").
+      rewrite /task_Join. iApply ("IH" with "[Htoken] HΦ").
       iExists _,_,_; iFrame "Htask"; eauto.
     - iDestruct "Hstatus" as (v) "(>Hstate & >Hres & HQ)".
       wp_load.
       iMod ("Hcl" with "[Hstate Hres HQ]") as "_".
       { iNext; iRight; iLeft. iExists _; iFrame. }
       iModIntro. wp_op. wp_if.
-      rewrite /task_Join. iApply ("IH" with "[$Htoken] HΦ").
+      rewrite /task_Join. iApply ("IH" with "[Htoken] HΦ").
       iExists _,_,_; iFrame "Htask"; eauto.
     - iDestruct "Hstatus" as (v) "(>Hstate & >Hres & #HFIN & HQ)".
       wp_load.
@@ -264,8 +264,7 @@ Section contents.
       iMod (shoot v γ with "[Htoken Htoken2]") as "#Hshot".
       { iCombine "Htoken Htoken2" as "?". done. }
       iMod ("Hcl" with "[Hstate Hres]") as "_".
-      { iNext. iRight. iRight. iExists _. iFrame. iFrame "HFIN".
-        iRight. eauto. }
+      { iNext. iRight. iRight. iFrame "#∗". }
       iModIntro. wp_op. wp_if. wp_bind (!#res)%E.
       iInv (N.@"task") as "[>(Hstate & Hres & Hpending & HINIT)|[Hstatus|Hstatus]]" "Hcl".
       { iExFalso. iApply (shot_not_pending with "Hshot Hpending"). }
diff --git a/theories/lecture_notes/lists.v b/theories/lecture_notes/lists.v
index 63ccdae5d6aca935a3501a3dcd47e93b39e40fa3..6e12ae8b338298a56f6988e628619e0b79c55114 100644
--- a/theories/lecture_notes/lists.v
+++ b/theories/lecture_notes/lists.v
@@ -76,9 +76,9 @@ Proof.
   - eauto.
   - by iIntros "(? & _)".
   - iDestruct 1 as (l hd') "(? & ? & H & ?)". rewrite IHxs. iDestruct "H" as "(H_isListxs' & ?)".
-    iFrame. iExists l, hd'. iFrame.
+    iFrame.
   - iDestruct 1 as "(H_isList & ? & H)". iDestruct "H_isList" as (l hd') "(? & ? & ?)".
-    iExists l, hd'. rewrite IHxs. iFrame.
+    iFrame. rewrite IHxs. iFrame.
 Qed.
 
 (* The predicate
@@ -246,7 +246,7 @@ Proof.
      wp_match. do 2 (wp_load; wp_proj; wp_let). wp_op.
      wp_store. iApply ("IH" with "Hxs").
      iNext. iIntros (w) "H'". iApply "H". iDestruct "H'" as "[Hw Hislist]".
-     iFrame. iExists l, hd'. iFrame. done.
+     iFrame. done.
 Qed.
 
 
@@ -328,8 +328,7 @@ Proof.
     iApply ("IH" with "H_isList H_Pxs' H_Iempty [H_l H_Px H_inv]").
     iNext. iIntros (r) "(H_isListxs' & H_Ixs')".
     iApply ("H_f" with "[$H_Ixs' $H_Px] [H_inv H_isListxs' H_l]").
-    iNext. iIntros (r') "H_inv'". iApply "H_inv". iFrame.
-    iExists l, hd'. by iFrame.
+    iNext. iIntros (r') "H_inv'". iApply "H_inv". iFrame. done.
 Qed.
 
 Lemma foldr_spec_PPI P I (f a hd : val) (xs : list val) :
diff --git a/theories/lecture_notes/stack.v b/theories/lecture_notes/stack.v
index 0ce8e928441ac9dff724964fe3d84db9ba9c8a11..7a572cc0c880fbebf72470b1e24f990404e05a49 100644
--- a/theories/lecture_notes/stack.v
+++ b/theories/lecture_notes/stack.v
@@ -89,8 +89,7 @@ Section stack_spec.
     wp_store.
     iApply "HΦ".
     iExists â„“, (SOMEV #â„“'); iFrame.
-    iSplitR; first done.
-    iExists â„“', hd; by iFrame.
+    iSplitR; done.
   Qed.
 
   Lemma pop_spec_nonempty s (x : val) xs:
@@ -183,8 +182,7 @@ Proof.
   wp_store.
   iApply "HΨ".
   iExists â„“, (SOMEV #â„“'); iFrame.
-  iSplitR; first done.
-  iExists â„“', x, hd; by iFrame.
+  iSplitR; done.
 Qed.
 
 Lemma pop_ownership_spec_nonempty s Φ Φs:
diff --git a/theories/locks/array_based_queuing_lock/abql.v b/theories/locks/array_based_queuing_lock/abql.v
index d91eff4e779b4eb988009aa4a966fb618bb0f295..95ddb4becaf216823c6e5aa00079836d035ec0a6 100644
--- a/theories/locks/array_based_queuing_lock/abql.v
+++ b/theories/locks/array_based_queuing_lock/abql.v
@@ -385,8 +385,7 @@ Section proof.
       - iLeft. iFrame. rewrite Nat.Div0.mod_0_l //. }
     wp_pures.
     iApply "Post".
-    rewrite /is_lock. iFrame.
-    iExists _, _. auto.
+    rewrite /is_lock. iFrame. auto.
   Qed.
 
   Lemma rem_mod_eq (x y : nat) : (0 < y) → (x `rem` y)%Z = x `mod` y.
diff --git a/theories/locks/freeable_lock/freeable_logatom_lock.v b/theories/locks/freeable_lock/freeable_logatom_lock.v
index 97e795fba7e4352a974ef2de50aa2322f3c2038d..9c4003644169d15cd06fdebae7af4cb1d035a089 100644
--- a/theories/locks/freeable_lock/freeable_logatom_lock.v
+++ b/theories/locks/freeable_lock/freeable_logatom_lock.v
@@ -137,8 +137,7 @@ Section tada.
         rewrite {1}/sum_loans /= map_fold_sum_loans_add Qp.div_2. done.
       - iApply big_sepM_insert; first done. iFrame "Hloans".
         iExists _. by iFrame. }
-    iModIntro. iExists _. iFrame.
-    iExists _, _. by iFrame.
+    iModIntro. iExists _. iFrame "#∗".
   Qed.
 
   Local Lemma return_lock_loan γ q Q :
diff --git a/theories/logatom/conditional_increment/cinc.v b/theories/logatom/conditional_increment/cinc.v
index e8d0d507d69fd1c8decae98d66fa5460e31010c8..8d57444d477a00302292155111661eaa6d42080e 100644
--- a/theories/logatom/conditional_increment/cinc.v
+++ b/theories/logatom/conditional_increment/cinc.v
@@ -298,11 +298,10 @@ Section conditional_counter.
     iSplitL "Hl_ghost_inv Hl_ghost Q Hp' Hl".
     (* Update state to Done. *)
     { iNext. iExists _. iFrame "Hp'". iRight. unfold done_state.
-      iFrame "#∗". iDestruct "Hl_ghost_inv" as (v) "Hl_ghost_inv".
-      iDestruct (pointsto_agree with "Hl_ghost Hl_ghost_inv") as %<-.
-      iSplitR "Hl"; iExists _; iFrame. }
+      iDestruct "Hl_ghost_inv" as (v) "Hl_ghost_inv".
+      iDestruct (pointsto_agree with "Hl_ghost Hl_ghost_inv") as %<-. iFrame "#∗". }
     iModIntro. iSplitR "HQ".
-    { iNext. iDestruct "Hc" as "[Hc1 Hc2]".
+    { iNext. iDestruct "Hc" as "[Hc1 Hc2]". 
       iExists l_new, _, (Quiescent n). iFrame. }
     wp_seq. iApply "HQ".
     iApply state_done_extract_Q; done.
diff --git a/theories/logatom/counter_with_backup/counter_proof.v b/theories/logatom/counter_with_backup/counter_proof.v
index 7c1ec6cbafa97d372fa3ed7d329330f314385d14..ad53ab7e03ebd98beca4403ff817621cdc2ccc44 100644
--- a/theories/logatom/counter_with_backup/counter_proof.v
+++ b/theories/logatom/counter_with_backup/counter_proof.v
@@ -232,8 +232,7 @@ Section counter_proof.
       rewrite bool_decide_decide; destruct decide; first lia.
       iDestruct "Hget" as (O) "[Hmap Hset]".
       iMod (logicall_execute_gets_set with "[$Hc $Hset]") as "[Hc Hset]".
-      iModIntro. iFrame. iSplitL "Hset Hmap".
-      { iExists O. iFrame. }
+      iModIntro. iFrame.
       iApply (big_sepM_impl with "Hgets"). iModIntro.
       iIntros (k γ' Hel). iDestruct 1 as (O') "(Hmap & Hset)".
       iExists O'. iFrame. iApply (big_sepS_impl with "Hset").
@@ -245,9 +244,9 @@ Section counter_proof.
     - eapply delete_notin in Hlook. rewrite -Hlook. iModIntro. iFrame.
       iApply (big_sepM_impl with "Hgets"). iModIntro.
       iIntros (k γ' Hel). iDestruct 1 as (O') "(Hmap & Hset)".
-      iExists O'. iFrame. iApply (big_sepS_impl with "Hset").
+      iFrame. iApply (big_sepS_impl with "Hset").
       iModIntro. iIntros ([γ1' γ2'] Hel'). iDestruct 1 as (Ψ) "(I' & Hvar & Hcred)".
-      iExists Ψ. iFrame "I'". rewrite !bool_decide_decide.
+      iFrame "I'". rewrite !bool_decide_decide.
       destruct decide, decide; [iFrame| | lia | iFrame].
       assert (S n = k) as Heq by lia. rewrite Heq lookup_delete in Hel.
       naive_solver.
@@ -288,7 +287,6 @@ Section counter_proof.
     iSplitR ""; last done.
     iSplit; first done. rewrite !big_sepM_insert //.
     iFrame. iSplitR; first eauto with iFrame.
-    iExists ∅. iFrame.
     rewrite big_sepS_empty. done.
   Qed.
 
@@ -483,7 +481,7 @@ Section counter_proof.
     awp_apply load_spec.
     iInv "I" as (G P n_b n_p) "(>%Hn & >Hb & >Hp & >Hcnt & >Hprim & Hrest)".
     iAaccIntro with "Hp".
-    { iIntros "?". iModIntro. rewrite /counter_inv /counter_inv_inner. iFrame "Cnt Hone". iFrame. iNext. iExists G, P, n_b, n_p. eauto with iFrame. }
+    { iIntros "?". iModIntro. rewrite /counter_inv /counter_inv_inner. by iFrame. }
     iIntros "Hp". iDestruct (mono_nat_auth_own_agree with "Hcnt Cnt") as %[_ ->].
     iDestruct (mono_nat_lb_own_get with "Hprim") as "#Hn_p".
     iModIntro. iSplitR "Cnt Cnt2 Hone".
@@ -495,8 +493,7 @@ Section counter_proof.
     iDestruct (mono_nat_auth_own_agree with "Hcnt Cnt") as %[_ ->].
     iDestruct (mono_nat_lb_own_valid with "Hprim Hn_p") as %[_ Hle].
     iAaccIntro with "Hb".
-    { iIntros "Hb". iFrame. iModIntro. iNext. rewrite /counter_inv /counter_inv_inner.
-      iExists G, P, n, n_p'. iFrame. iPureIntro. lia. }
+    { iIntros "Hb". iFrame. iPureIntro. lia. }
     iIntros "Hb". iMod (lc_fupd_elim_later with "Hone Hrest") as "(HG & #Hlook & HP & Hgets & Hputs)".
     iMod (logically_execute_gets_and_puts _ _ _ _ _ n_p with "Hputs Hgets Cnt Cnt2 Hcnt") as "(Hputs & Hgets & Cnt & Cnt2 & Hcnt)"; first (split; by eauto).
     iModIntro. iSplitR "Cnt Cnt2".
@@ -539,7 +536,7 @@ Section counter_proof.
     awp_apply load_spec.
     iInv "I" as (G P n_b n_p) "(>% & >Hb & >Hp & Hrest)".
     iAaccIntro with "Hp".
-    { iIntros "Hp". iModIntro. iFrame. iNext. rewrite /counter_inv /counter_inv_inner. iExists G, P, n_b, n_p. eauto with iFrame. }
+    { iIntros "Hp". iModIntro. iFrame. eauto. }
     iIntros "Hp". iMod (lc_fupd_elim_later with "Hone' Hrest") as "(Hcnt & Hprim & HG & #Hlook & HP & Hget & Hput)".
      assert (n_b = n_p ∨ n_b < n_p) as [->|Hlt] by lia.
     - (* we are reading the latest value, we can linearize now *)
@@ -576,7 +573,7 @@ Section counter_proof.
     awp_apply load_spec.
     iInv "I" as (G P n_b n_p) "(>% & >Hb & >Hp & Hrest)".
     iAaccIntro with "Hb".
-    { iIntros "Hb". iModIntro. iFrame. iNext. rewrite /counter_inv /counter_inv_inner. iExists G, P, n_b, n_p. eauto with iFrame. }
+    { iIntros "Hb". iModIntro. by iFrame. }
     iIntros "Hb".
      iMod (lc_fupd_elim_later with "Hone' Hrest") as "(Hcnt & Hprim & HG & #Hlook & HP & Hget & Hput)".
      iMod "AU" as (n) "[[Hc Hex] [_ Hclose]]".
@@ -597,7 +594,7 @@ Section counter_proof.
     awp_apply faa_spec.
     iInv "I" as (G P n_b n_p) "(>% & >Hb & >Hp & Hrest)".
     iAaccIntro with "Hp".
-    { iIntros "Hp". iModIntro. iFrame. iNext. rewrite /counter_inv /counter_inv_inner. iExists G, P, n_b, n_p. eauto with iFrame. }
+    { iIntros "Hp". iModIntro. by iFrame. }
     iIntros "Hp". iMod (lc_fupd_elim_later with "Hone' Hrest") as "(Hcnt & Hprim & HG & #Hlook & HP & Hget & Hput)".
     iMod (counter_inv_inner_register_put _ _ (γ_cnt, γ_ex) with "AU Hone Hb [Hp] Hcnt Hprim HG Hlook HP Hget Hput") as "Hupd"; first lia.
     { replace (n_p + 1)%Z with (S n_p : Z) by lia. iExact "Hp". }
diff --git a/theories/logatom/flat_combiner/flat.v b/theories/logatom/flat_combiner/flat.v
index b6a6f4eb8cd09170aa38d8808b0639154b46f1d7..0a3cabc7ac2e833674e8f2b1e685d1ff6c37214c 100644
--- a/theories/logatom/flat_combiner/flat.v
+++ b/theories/logatom/flat_combiner/flat.v
@@ -126,13 +126,10 @@ Section proof.
     iModIntro. wp_let. wp_bind (push _ _).
     iMod (inv_alloc N _ (p_inv R γm γr (γx, γ1, γ3, γ4, γq) p)
           with "[-HΦ Hx2 Ho3]") as "#HRx"; first eauto.
-    { iNext. iRight. iLeft. iExists f, x. iFrame.
-      iExists (λ _, P), (λ _ v, Q v).
-      iFrame. iFrame "#". }
+    { iNext. iRight. iLeft. iExists f, x. iFrame "#∗". }
     iApply (push_spec N (p_inv' R γm γr) s #p
             with "[-HΦ Hx2 Ho3]")=>//.
-    { iFrame "#". iExists (γx, γ1, γ3, γ4, γq), p.
-      iSplitR; first done. iFrame "#". }
+    { by iFrame "#". }
     iNext. iIntros "?".
     wp_seq. iApply ("HΦ" $! p (γx, γ1, γ3, γ4, γq)).
     iFrame. by iFrame "#".
@@ -172,7 +169,7 @@ Section proof.
         wp_store. iDestruct (m_frag_agree' with "Hx Hx2") as "[Hx %]".
         subst. rewrite Qp.div_2. iMod ("Hclose" with "[-HR Hor HΦ]").
         { iNext. iDestruct "Hp" as "[Hp1 Hp2]". iRight. iRight.
-          iRight. iExists _, v. iFrame. iExists Q. iFrame. }
+          iRight. iExists _, v. by iFrame. }
         iApply "HΦ". iFrame. done.
       * iDestruct "Hp" as (? ?) "[? Hs]". iDestruct "Hs" as (?) "(_ & _ & _ & >Ho1' & _)".
         iApply excl_falso. iFrame.
@@ -181,7 +178,7 @@ Section proof.
     - destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (x' y) "[Hp Hs]".
         iDestruct "Hs" as (Q) "(>Hx & HoQ & HQxy & >Ho1 & >Ho4)".
         wp_load. iMod ("Hclose" with "[-HΦ HR Hor]").
-        { iNext. iRight. iRight. iRight. iExists x', y. iFrame. iExists Q. iFrame. }
+        { iNext. iRight. iRight. iRight. iExists x', y. by iFrame. }
         iModIntro. wp_match. iApply "HΦ". by iFrame.
   Qed.
 
@@ -230,7 +227,7 @@ Section proof.
     iDestruct "H" as (xs' hd') "[>Hs #Hxs]".
     wp_load.
     iMod ("Hclose" with "[Hs]").
-    { iNext. iFrame. iExists xs', hd'. by iFrame. }
+    { iFrame "#∗". }
     iModIntro. wp_let. wp_bind (treiber.iter _ _).
     iApply wp_wand_r. iSplitL "HR Ho2".
     { iApply (loop_iter_doOp_spec R _ _ _ _ (λ _, own γr (Excl ()) ∗ R)%I with "[-]")=>//.
@@ -262,8 +259,7 @@ Section proof.
       iFrame "#". wp_seq. iApply ("IH" with "Ho3"); eauto.
     + iDestruct "Hp" as (f x) "(Hp & Hx & Ho2 & Ho4)".
       wp_load. iMod ("Hclose" with "[-Ho3 HΦ]") as "_".
-      { iNext. (* FIXME: iFrame here divergses, with an enormous TC trace *)
-        iRight. iRight. iLeft. iExists f, x. iFrame. }
+      { iNext. iRight. iRight. iLeft. iFrame. }
       iModIntro. wp_match.
       wp_apply try_srv_spec=>//.
       iFrame "#". wp_seq. iApply ("IH" with "Ho3"); eauto.
@@ -271,8 +267,7 @@ Section proof.
       iDestruct "Hs'" as (Q) "(>Hx & HoQ & HQ & >Ho1 & >Ho4)".
       wp_load. iMod ("Hclose" with "[-Ho4 HΦ Hx HoQ HQ]").
       { iNext. iLeft. iExists y. iFrame. }
-      iModIntro. wp_match. iApply ("HΦ" with "[-]"). iFrame.
-      iExists Q. iFrame.
+      iModIntro. wp_match. iApply ("HΦ" with "[-]"). by iFrame.
   Qed.
 
   Lemma mk_flat_spec (γm: gname): mk_syncer_spec mk_flat.
diff --git a/theories/logatom/flat_combiner/peritem.v b/theories/logatom/flat_combiner/peritem.v
index 6eabb56fa2f6293de69657f527ee2f511ddec49e..7a913e4466bb722139618fcddeb5c26fd2ac225c 100644
--- a/theories/logatom/flat_combiner/peritem.v
+++ b/theories/logatom/flat_combiner/peritem.v
@@ -46,8 +46,7 @@ Section proofs.
     iMod (pointsto_persist with "Hl") as "#Hl".
     wp_alloc s as "Hs".
     iAssert (∃ xs, is_bag_R N R xs s)%I with "[-HΦ]" as "Hxs".
-    { iFrame. iExists [], l.
-      iFrame. simpl. eauto. }
+    { iFrame. iExists []. eauto. }
     iMod (inv_alloc N _ (∃ xs : list val, is_bag_R N R xs s)%I with "[-HΦ]") as "#?"; first eauto.
     iApply "HΦ". iFrame "#". done.
   Qed.
@@ -61,7 +60,7 @@ Section proofs.
     iInv N as "H1" "Hclose".
     iDestruct "H1" as (xs hd) "[>Hs H1]".
     wp_load. iMod ("Hclose" with "[Hs H1]").
-    { iNext. iFrame. iExists xs, hd. iFrame. }
+    { iFrame. }
     iModIntro. wp_let. wp_alloc l as "Hl".
     wp_let. wp_bind (CmpXchg _ _ _)%E.
     iInv N as "H1" "Hclose".
@@ -71,13 +70,11 @@ Section proofs.
       iMod (pointsto_persist with "Hl") as "#Hl".
       iMod (inv_alloc N _ (R x) with "[HRx]") as "#HRx"; first eauto.
       iMod ("Hclose" with "[Hs Hl H1]").
-      { iNext. iFrame. iExists (x::xs'), l.
-        iFrame. simpl. iExists hd'. iFrame.
-        by iFrame "#". }
+      { iExists (x::xs'). iFrame "#∗". }
       iModIntro. wp_pures. by iApply "HΦ".
     - wp_cmpxchg_fail.
       iMod ("Hclose" with "[Hs H1]").
-      { iNext. iFrame. iExists (xs'), hd'. iFrame. }
+      { iFrame. }
       iModIntro. wp_pures. iApply ("IH" with "HRx").
       by iNext.
   Qed.
diff --git a/theories/logatom/herlihy_wing_queue/hwq.v b/theories/logatom/herlihy_wing_queue/hwq.v
index 23cfae5934e267495ad040e3cd172a5cd1ecfad3..901a7f54f324d99a7492e010a39b12cfcdaba311 100644
--- a/theories/logatom/herlihy_wing_queue/hwq.v
+++ b/theories/logatom/herlihy_wing_queue/hwq.v
@@ -1512,7 +1512,7 @@ Proof.
     pose (cont := NoCont (map (λ i, (i, [])) pvs)).
     iNext. iExists 0, pvs, [], [], cont, ∅, ∅.
     rewrite array_content_empty Nat2Z.id fmap_empty /=.
-    iFrame. iSplitL. { iExists rs. by iFrame. }
+    iFrame.
     repeat (iSplit; first done). iPureIntro.
     repeat split_and; try done.
     - intros i. split; intros Hi; [ by lia | by inversion Hi].
@@ -2160,8 +2160,7 @@ Proof.
         intros ->. apply Hpref in Hk as (H1 & H2).
         rewrite Hi_free in H1. inversion H1. }
       iSplitL "Hbig Hpend_tok_i AU".
-      { iApply big_sepM_insert; first done. iFrame. iSplit; first done.
-        iExists (Φ #()). iFrame. done. }
+      { iApply big_sepM_insert; first done. iFrame "#∗". }
       iPureIntro. subst new_slots. repeat split_and; try done.
       - intros k. destruct sz as [|sz]; first by lia.
         split; intros Hk.
@@ -2675,8 +2674,6 @@ Proof.
         iNext. iExists back', new_pvs, new_pref, rest, cont', slots, new_deqs.
         subst new_deqs. iFrame. iSplitL "Hâ„“_ar".
         { rewrite array_content_dequeue; [ done | by lia | done ]. }
-        iSplitL "Hp".
-        { iExists rs'. by iFrame "Hp". }
         iPureIntro. repeat split_and; try done.
         - intros k. split; intros Hk; first by apply Hstate.
           intros Hk_in_deqs. apply elem_of_union in Hk_in_deqs.
@@ -2743,8 +2740,8 @@ Proof.
       [ by rewrite Hi | by rewrite Hi | by right | ]. iIntros "Hâ„“a" (rs' ->) "Hp".
     (* We can close the invariant. *)
     iModIntro. iSplitR "AU Hback_snap Hi2_lower_bound".
-    { iNext. iExists _, _, _, _, cont', _, _. iFrame. iSplit; last done.
-      iExists rs'. rewrite Hpvs /= decide_True; last by lia. by iFrame. }
+    { iNext. iExists _, _, _, _, cont', _, _. iFrame. iSplit; last done. iPureIntro.
+      rewrite Hpvs /= decide_True; last by lia. done. }
     (* And conclude using the loop induction hypothesis. *)
     wp_pures. assert (S n - 1 = n)%Z as -> by lia. iClear "Hval_wit_i".
     iApply ("IH_loop" with "[] [] AU Hback_snap").
diff --git a/theories/logrel/F_mu_ref_conc/binary/examples/stack/refinement.v b/theories/logrel/F_mu_ref_conc/binary/examples/stack/refinement.v
index 7e300a208bc234f2bfe5e3f7526bd2ecf236ccce..f6ceba91704819d0561037cf5b08105190840073 100644
--- a/theories/logrel/F_mu_ref_conc/binary/examples/stack/refinement.v
+++ b/theories/logrel/F_mu_ref_conc/binary/examples/stack/refinement.v
@@ -303,9 +303,8 @@ Section Stack_refinement.
         iApply ("Hlat" $! istk6 zn2 with "[Hj] [HLK]"); trivial.
         rewrite StackLink_unfold; iModIntro; simpl.
         iDestruct "HLK" as "[Histk6 [HLK|HLK]]";
-          iExists istk6, w'; iSplit; auto; iFrame "#".
-        iRight. iDestruct "HLK" as (? ? ? ?) "(?&?&?&?)".
-        iExists _, _, _, _; iFrame "#".
+          iExists istk6, w'; iSplit; auto. iFrame "Histk6".
+        iDestruct "HLK" as (? ? ? ?) "(?&?&?&?)". iFrame "#".
   Qed.
 End Stack_refinement.
 
diff --git a/theories/spanning_tree/spanning.v b/theories/spanning_tree/spanning.v
index eadae373d5ae2b382364c72eb83e115bb1b1f3fe..64ee1f90c7aad558fd68c47074bb2e3f3472ae8d 100644
--- a/theories/spanning_tree/spanning.v
+++ b/theories/spanning_tree/spanning.v
@@ -56,7 +56,7 @@ Section Helpers.
     wp_load.
     iDestruct "Hil1" as %Hil1. iDestruct "Hil2" as %Hil2.
     iDestruct (graph_close with "[Hi3 Hil3 Hil4]") as "Hi3"; eauto.
-    { iFrame. iExists _; eauto. iSplitR; eauto. iExists _; by iFrame. }
+    { by iFrame. }
     iMod ("Hcl" with "[Hi1 Hi2 Hi3 Hi4]") as "_".
     { iNext. unfold graph_inv at 2. iExists _; iFrame; auto. }
     iModIntro. wp_proj. wp_let.
@@ -78,7 +78,7 @@ Section Helpers.
     - wp_cmpxchg_fail.
       iDestruct (graph_close with "[Hi3 Hil3 Hil4]") as "Hi3";
       eauto.
-      { iFrame. iExists _; eauto. iSplitR; eauto. by iExists _; iFrame. }
+      { by iFrame. }
       iMod (already_marked with "Hi2") as "[Hi2 Hxm]"; [|iFrame "Hxm"].
       { by eapply in_dom_of_graph. }
       iMod ("Hclose" with "[Hi1 Hi2 Hi3]") as "_".
@@ -93,7 +93,7 @@ Section Helpers.
       erewrite delete_marked.
       iDestruct (auth_own_graph_valid with "Hi1") as %Hvl'.
       iDestruct (graph_close with "[Hi3 Hil3 Hil4]") as "Hi3".
-      { iFrame. iExists (_, _). iSplitR; [| iExists _; iFrame]; trivial.
+      { iFrame "Hi3". iExists (_, _). iFrame.
           rewrite mark_update_lookup; eauto. }
       iMod ("Hclose" with "[Hi1 Hi2 Hi3]") as "_".
       + iNext; unfold graph_inv at 2. iExists _; iFrame.
@@ -142,8 +142,7 @@ Section Helpers.
       as %Heq; try by iFrame.
     pose proof Hil1 as Hil1'. rewrite Heq in Hil1' Hvl.
     rewrite mark_update_lookup in Hil1'; trivial.
-    iDestruct (graph_close with "[Hi3 Hil3 Hil4]") as "Hi3"; [iFrame|].
-    { iExists _; iSplitR; auto. iExists _; by iFrame. }
+    iDestruct (graph_close with "[Hi3 Hil3 Hil4]") as "Hi3"; [by iFrame|].
     iMod ("Hclose" with "[Hi1 Hi2 Hi3]") as "_".
     { iNext. unfold graph_inv at 2. iExists _; iFrame; auto. }
     iFrame. inversion Hil1'; subst u'; simpl.
@@ -368,14 +367,13 @@ Section Helpers.
       iCombine "Hx" "Hxlr" as "Hx". rewrite -graph_divide.
       destruct u1; destruct u2; inversion Hl1eq; inversion Hl2eq; subst.
       iModIntro. iFrame; iLeft. iSplit; [trivial|].
-      iExists _; iSplit; [trivial|]. iFrame.
-      iDestruct (own_graph_valid with "Hx") as %Hvl.
-      iExists ({[l := Excl (Some l1, Some l2)]} â‹… (G1 â‹… G2)).
+      iExists _; iSplit; [trivial|]. iFrame "Hm".
+      iDestruct (own_graph_valid with "Hx") as %Hvl. iFrame "Hx".
       iDestruct (front_marked _ _ _ _ (Some l1, Some l2) _ _ G1 G2 with
       "[ml1 ml2 Hfml Hfmr]") as (mr)"[Hfr Hfm]"; eauto. iDestruct "Hfr" as %Hfr.
-      iExists mr.
+      iFrame "Hfm".
       unshelve iExists _; [eapply maximally_marked_tree_both; eauto|].
-      iFrame. iSplit; try iPureIntro; eauto.
+      iSplit; try iPureIntro; eauto.
       { rewrite dom_op dom_singleton elem_of_union elem_of_singleton; by left. }
       split; auto.
       { eapply maximally_marked_tree_both; eauto. }
@@ -393,9 +391,8 @@ Section Helpers.
       iCombine "Hx" "Hxlr" as "Hx". rewrite -graph_divide.
       wp_seq. iModIntro.
       iFrame; iLeft. iSplit; [trivial|].
-      iExists _; iSplit; [trivial|]. iFrame.
-      iDestruct (own_graph_valid with "Hx") as %Hvld.
-      iExists ({[l := Excl (u1, None)]} â‹… G1).
+      iExists _; iSplit; [trivial|]. iFrame "Hm".
+      iDestruct (own_graph_valid with "Hx") as %Hvld. iFrame "Hx".
       destruct u1; inversion Hl1eq; subst.
       iDestruct (front_marked _ _ _ _ (Some l1, None) _ ∅ G1 ∅ with
       "[ml1 Hvr Hfml]") as (mr)"[Hfr Hfm]"; eauto.
@@ -405,10 +402,9 @@ Section Helpers.
         [iDestruct "Hvr" as %Hvr; inversion Hvr|
          iDestruct "Hvr" as (l2) "[Hvreq Hvr]"; iDestruct "Hvreq" as %Hvreq;
          by inversion Hvreq]. }
-      iDestruct "Hfr" as %Hfr. rewrite right_id_L in Hfr.
-      iExists mr.
+      iDestruct "Hfr" as %Hfr. rewrite right_id_L in Hfr. iFrame "Hfm".
       unshelve iExists _; [eapply maximally_marked_tree_left; eauto|].
-      iFrame. iSplit; try iPureIntro; eauto.
+      iSplit; try iPureIntro; eauto.
       { rewrite dom_op dom_singleton elem_of_union elem_of_singleton; by left. }
       split; auto.
       { eapply maximally_marked_tree_left; eauto. }
@@ -426,9 +422,8 @@ Section Helpers.
       iCombine "Hx" "Hxlr" as "Hx". rewrite -graph_divide.
       wp_seq. wp_proj. wp_op. wp_if. wp_seq. iModIntro.
       iFrame; iLeft. iSplit; [trivial|].
-      iExists _; iSplit; [trivial|]. iFrame.
-      iDestruct (own_graph_valid with "Hx") as %Hvld.
-      iExists ({[l := Excl (None, u2)]} â‹… G2).
+      iExists _; iSplit; [trivial|]. iFrame "Hm".
+      iDestruct (own_graph_valid with "Hx") as %Hvld. iFrame "Hx".
       destruct u2; inversion Hl2eq; subst.
       iDestruct (front_marked _ _ _ _ (None, Some l2) ∅ _ ∅ G2 with
       "[ml2 Hvl Hfmr]") as (mr)"[Hfr Hfm]"; eauto.
@@ -439,9 +434,9 @@ Section Helpers.
          iDestruct "Hvl" as (l1) "[Hvleq Hvl]"; iDestruct "Hvleq" as %Hvleq;
          by inversion Hvleq]. }
       iDestruct "Hfr" as %Hfr. rewrite left_id_L in Hfr.
-      iExists mr.
+      iFrame "Hfm".
       unshelve iExists _; [eapply maximally_marked_tree_right; eauto|].
-      iFrame. iSplit; try iPureIntro; eauto.
+      iSplit; try iPureIntro; eauto.
       { rewrite dom_op dom_singleton elem_of_union elem_of_singleton; by left. }
       split; auto.
       { eapply maximally_marked_tree_right; eauto. }
@@ -459,9 +454,8 @@ Section Helpers.
       iCombine "Hx" "Hxlr" as "Hx". rewrite -graph_divide.
       wp_seq. iModIntro.
       iFrame; iLeft. iSplit; [trivial|].
-      iExists _; iSplit; [trivial|]. iFrame.
-      iDestruct (own_graph_valid with "Hx") as %Hvld.
-      iExists ({[l := Excl (None, None)]} ⋅ ∅).
+      iExists _; iSplit; [trivial|]. iFrame "Hm".
+      iDestruct (own_graph_valid with "Hx") as %Hvld. iFrame "Hx".
       iDestruct (front_marked _ _ _ _ (None, None) ∅ ∅ ∅ ∅ with
       "[Hvr Hvl]") as (mr)"[Hfr Hfm]"; eauto.
       { rewrite dom_empty_L; apply front_empty. }
@@ -477,10 +471,10 @@ Section Helpers.
             iDestruct "Hvreq" as %Hvreq; inversion Hvreq);
           iFrame; by repeat iSplit. }
       iDestruct "Hfr" as %Hfr. rewrite left_id_L in Hfr.
-      iExists mr.
+      iFrame "Hfm".
       rewrite right_id_L. rewrite right_id_L in Hvld Hfr.
       unshelve iExists _; [eapply maximally_marked_tree_none; eauto|].
-      iFrame. iSplit; try iPureIntro; eauto.
+      iSplit; try iPureIntro; eauto.
       { by rewrite dom_singleton elem_of_singleton. }
       split; auto.
       { eapply maximally_marked_tree_none; eauto. }