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/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/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/counter_with_backup/counter_proof.v b/theories/logatom/counter_with_backup/counter_proof.v
index 7482f654cce38a8316980eae1813ddd328191a0b..ad53ab7e03ebd98beca4403ff817621cdc2ccc44 100644
--- a/theories/logatom/counter_with_backup/counter_proof.v
+++ b/theories/logatom/counter_with_backup/counter_proof.v
@@ -493,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".
@@ -537,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 *)
@@ -574,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]]".
@@ -595,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 ee5dbc4a22b76136dc90d41778f3f5b7643b4b1f..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].
@@ -2674,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.
@@ -2742,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").