diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 5b4e7d9d56547f38225f88ea70562aa92aeb1826..e6111801d1d9b3b4ce856412a32fdf36fccb5fd9 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -189,7 +189,7 @@ Section arc.
     iMod (own_alloc ((● (Some $ Cinl ((1/2)%Qp, xH, None), O) ⋅
                       â—¯ (Some $ Cinl ((1/2)%Qp, xH, None), O))))
       as (γ) "[H● H◯]"; first by apply auth_both_valid_discrete.
-    iExists _, _. iFrame. iApply inv_alloc. iExists _. iFrame. iExists _. iFrame.
+    iFrame. iApply inv_alloc. iExists _. iFrame.
     rewrite Qp.div_2. auto.
   Qed.
 
@@ -314,7 +314,7 @@ Section arc.
       { by apply auth_update_alloc, prod_local_update_2,
               (op_local_update_discrete _ _ (1%nat)). }
       iMod ("Hclose1" with "[-Hown' HP HΦ]") as "_".
-      { iExists _. iFrame. iExists _.
+      { iExists _. iFrame.
         rewrite Z.add_comm -(Nat2Z.inj_add 1) /=. auto with iFrame. }
       iModIntro. wp_case. iApply "HΦ". iFrame.
     - destruct wlock.
@@ -529,7 +529,7 @@ Section arc.
         iMod (own_update_2 _ _ _ _ with "H● Hown") as "H●".
         { apply auth_update_dealloc, prod_local_update_1, @cancel_local_update_unit, _. }
         iMod ("Hclose" with "[- HΦ]") as "_".
-        { iExists _. iFrame. iExists (q + q'')%Qp. iCombine "HP1 HP1'" as "$".
+        { iExists _. iCombine "HP1 HP1'" as "HP". iFrame "H●". iFrame.
           iSplit; last by destruct s.
           iIntros "!> !%". rewrite assoc -Hq''. f_equal. apply comm, _. }
         iModIntro. wp_case. wp_op; case_bool_decide; simplify_eq. by iApply "HΦ".
diff --git a/theories/lang/lib/spawn.v b/theories/lang/lib/spawn.v
index e2777f892571510e1d4cb86bc9ce8c70260ce518..40cd71babe0f85db77c1b1d16ee8b09fd8b1eb83 100644
--- a/theories/lang/lib/spawn.v
+++ b/theories/lang/lib/spawn.v
@@ -90,7 +90,7 @@ Proof.
     auto. }
   iDestruct "Hinv" as (b) "[>Hc _]". wp_write.
   iMod ("Hclose" with "[-HΦ]").
-  - iNext. iRight. iExists true. iFrame. iExists _. iFrame.
+  - iNext. iRight. iExists true. iFrame.
   - iModIntro. wp_seq. by iApply "HΦ".
 Qed.
 
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 945816ce2d4a65d06c6eabf5d9aaa3683faec8d2..93f6474431db6f04c63ea77d32bc672a27a6c9ac 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -140,13 +140,12 @@ Proof.
       first solve_ndisj.
     { by rewrite lookup_insert. }
     iFrame.
-    iApply "Hclose'". iExists _, _. iFrame. rewrite big_sepS_later.
-    iApply "Hclose''". iLeft. iFrame "%". iExists _, _. iFrame.
-    iExists _. iFrame.
+    iApply "Hclose'". iFrame. rewrite big_sepS_later.
+    iApply "Hclose''". iLeft. iFrame "% ∗".
     rewrite insert_insert -(fmap_insert _ _ _ Bor_in) insert_id //.
   - iRight. iMod (lft_dead_in_tok with "HA") as "[HA #H†]"; first done.
     iMod ("Hclose'" with "[-Hbor]") as "_".
-    + iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''". eauto.
+    + iFrame. rewrite big_sepS_later. iApply "Hclose''". eauto.
     + iMod (lft_incl_dead with "Hle H†"); first done. iFrame.
       iApply fupd_mask_subseteq. solve_ndisj.
 Qed.
@@ -175,7 +174,7 @@ Proof.
     iMod ("Hclose'" with "[-Hbor Hclose]") as "_".
     { iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
       iLeft. iFrame "%". iExists _, _. iFrame. }
-    iExists κ''. iFrame "#". iIntros "!> %Q HvsQ HQ". clear -HE.
+    iExists κ''. iFrame "Hle". iIntros "!> %Q HvsQ HQ". clear -HE.
     iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
     iDestruct (own_bor_auth with "HI Hbor") as %Hκ'.
     rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
@@ -208,11 +207,11 @@ Proof.
         - by rewrite big_sepM_delete.
         - by rewrite -fmap_None -lookup_fmap fmap_delete. }
       iMod ("Hclose'" with "[-Hbor Htok Hclose]") as "_".
-      { iExists _, _. iFrame. rewrite big_sepS_later /lft_bor_alive. iApply "Hclose''".
-        iLeft. iFrame "%". iExists _, _. iFrame. }
+      { iFrame. rewrite big_sepS_later /lft_bor_alive. iApply "Hclose''".
+        iLeft. iFrame "% ∗". }
       iMod ("Hclose" with "Htok") as "$". iExists κ''. iModIntro.
-      iSplit; first by iApply lft_incl_refl. iExists j. iFrame.
-      iExists Q. rewrite -(bi.iff_refl emp). auto.
+      iSplit; first by iApply lft_incl_refl. iFrame.
+      iExists Q. rewrite -(bi.iff_refl emp). eauto.
     + iDestruct "Hinv" as (?) "[Hinv _]". iDestruct "Hinv" as (B ?) "[>Hinv _]".
       iDestruct (own_bor_valid_2 with "Hinv Hbor")
         as %[(_ & <- & INCL%option_included)%singleton_included_l _]%auth_both_valid_discrete.
@@ -238,7 +237,7 @@ Proof.
   rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
           /lfts_inv /lft_inv /lft_inv_dead /lft_alive_in lft_inv_alive_unfold.
   iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >%]] Hclose'']".
-  - iLeft. iExists (i.1). iFrame "#".
+  - iLeft. iFrame "Hle".
     iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
     unfold lft_bor_alive, idx_bor_own.
     iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
@@ -261,18 +260,18 @@ Proof.
                 -fmap_None -lookup_fmap fmap_delete //. }
     rewrite own_bor_op. iDestruct "Hown" as "[H● H◯]".
     iMod ("Hclose'" with "[- Hâ—¯]"); last first.
-    { iModIntro. iExists (i.1). iSplit; first by iApply lft_incl_refl.
-      iExists j. iFrame. iExists Q. rewrite -(bi.iff_refl emp). auto. }
-    iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
-    iLeft. iFrame "%". iExists _, _. iFrame. iNext.
+    { iModIntro. iExists (i.1). iSplit; first by iApply lft_incl_refl. 
+      iFrame "Hs' ∗". rewrite -(bi.iff_refl emp). auto. }
+    iFrame. rewrite big_sepS_later. iApply "Hclose''".
+    iLeft. iFrame "%". iExists _, _.
     rewrite -!fmap_delete -fmap_insert -(fmap_insert _ _ _ Bor_in).
-    iExists _. iFrame "Hbox H●".
+    iFrame.
     rewrite big_sepM_insert; last first.
     { by rewrite -fmap_None -lookup_fmap fmap_delete. }
     by rewrite big_sepM_delete.
   - iRight. iMod (lft_dead_in_tok with "HA") as "[HA #H†]"; first done.
     iMod ("Hclose'" with "[-Hbor]") as "_".
-    + iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''". eauto.
+    + iFrame. rewrite big_sepS_later. iApply "Hclose''". eauto.
     + iMod (lft_incl_dead with "Hle H†") as "$"; first done.
       iApply fupd_mask_subseteq; first solve_ndisj.
 Qed.
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 310bcc8396b8da1b4f567115fe2a67884d8381f8..84949761aad28a44a71dbfd749f6d24404f7ea3a 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -42,8 +42,8 @@ Proof.
       simpl. iFrame. }
     iMod ("Hclose" with "[HA HI Hclose']") as "_"; [by iNext; iExists _, _; iFrame|].
     iSplitL "HBâ—¯ HsliceB".
-    + rewrite /bor /raw_bor /idx_bor_own. iModIntro. iExists γB. iFrame.
-      iExists P. rewrite -(bi.iff_refl emp). auto.
+    + rewrite /bor /raw_bor /idx_bor_own. iModIntro. iFrame.
+      rewrite -(bi.iff_refl emp). auto.
     + clear -HE. iIntros "!> H†".
       iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
       iDestruct ("HIlookup" with "HI") as %Hκ.
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 4541525e5ffd095614ed952f1adbe7ab9b9de723..72e655f4eedd659768c774fa188b386deff62d17 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -50,14 +50,12 @@ Proof.
                 -fmap_None -lookup_fmap fmap_delete //. }
     rewrite !own_bor_op. iDestruct "Hbor" as "[[H● H◯2] H◯1]".
     iAssert (&{κ}P)%I with "[H◯1 Hs1]" as "$".
-    { rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ1.
-      iFrame. iExists P. rewrite -(bi.iff_refl emp). auto. }
+    { rewrite /bor /raw_bor /idx_bor_own. iFrame "#∗". by rewrite -(bi.iff_refl emp). }
     iAssert (&{κ}Q)%I with "[H◯2 Hs2]" as "$".
-    { rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ2.
-      iFrame. iExists Q. rewrite -(bi.iff_refl emp). auto. }
-    iApply "Hclose". iExists A, I. iFrame. rewrite big_sepS_later.
-    iApply "Hclose'". iLeft. iFrame "%". iExists Pb', Pi. iFrame. iExists _.
-    rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "Hbox H●".
+    { rewrite /bor /raw_bor /idx_bor_own. iFrame "#∗". by rewrite -(bi.iff_refl emp). }
+    iApply "Hclose". iFrame. rewrite big_sepS_later.
+    iApply "Hclose'". iLeft.
+    rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "%∗".
     rewrite !big_sepM_insert /=.
     + by rewrite left_id -(big_sepM_delete _ _ _ _ EQB).
     + by rewrite -fmap_None -lookup_fmap fmap_delete.
@@ -66,9 +64,9 @@ Proof.
     iMod (raw_bor_fake with "Hdead") as "[Hdead Hbor1]"; first solve_ndisj.
     iMod (raw_bor_fake with "Hdead") as "[Hdead Hbor2]"; first solve_ndisj.
     iMod ("Hclose" with "[-Hbor1 Hbor2]") as "_".
-    { iExists A, I. iFrame. rewrite big_sepS_later. iApply "Hclose'".
-      iRight. iSplit; last by auto. iExists _. iFrame. }
-    unfold bor. iSplitL "Hbor1"; iExists _; eauto.
+    { iFrame. rewrite big_sepS_later. iApply "Hclose'".
+      iRight. by iFrame. }
+    unfold bor. by iFrame "#∗".
 Qed.
 
 Lemma bor_combine E κ P Q :
@@ -119,12 +117,11 @@ Proof.
     rewrite own_bor_op. iDestruct "Hbor" as "[H● H◯]".
     iAssert (&{κ}(P ∗ Q))%I with "[H◯ Hslice]" as "$".
     { rewrite /bor /raw_bor /idx_bor_own. iExists (κ1 ⊓ κ2).
-      iSplit; first by iApply (lft_incl_glb with "Hκ1 Hκ2").
-      iExists γ. iFrame. iExists _. iFrame. iNext. iModIntro.
+      iSplit; first by iApply (lft_incl_glb with "Hκ1 Hκ2"). iFrame. iNext. iModIntro.
       by iSplit; iIntros "[HP HQ]"; iSplitL "HP"; (iApply "HPP'" || iApply "HQQ'"). }
-    iApply "Hclose". iExists A, I. iFrame. rewrite big_sepS_later.
-    iApply "Hclose'". iLeft. iFrame "%". iExists Pb, Pi. iFrame. iExists _.
-    rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "Hbox H●".
+    iApply "Hclose". iFrame. rewrite big_sepS_later.
+    iApply "Hclose'". iLeft.
+    rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "%∗".
     rewrite !big_sepM_insert /=.
     + rewrite (big_sepM_delete _ _ _ _ EQB1) /=. iNext. simpl.
       rewrite [([∗ map] _ ∈ delete _ _, _)%I](big_sepM_delete _ _ j2 Bor_in) /=; last first.
@@ -134,8 +131,8 @@ Proof.
   - iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
     iMod (raw_bor_fake with "Hdead") as "[Hdead Hbor]"; first solve_ndisj.
     iMod ("Hclose" with "[-Hbor]") as "_".
-    { iExists A, I. iFrame. rewrite big_sepS_later. iApply "Hclose'".
-      iRight. iSplit; last by auto. iExists _. iFrame. }
-    unfold bor. iExists _. iFrame. iApply (lft_incl_glb with "Hκ1 Hκ2").
+    { iFrame. rewrite big_sepS_later. iApply "Hclose'".
+      iRight. by iFrame. }
+    unfold bor. iFrame. iApply (lft_incl_glb with "Hκ1 Hκ2").
 Qed.
 End borrow.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 2b3b0f4bc87ae962b09c1fa8a8e160f3bb94966b..3405d59a847828305cbe4bc60f0c316031a2ef5f 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -443,8 +443,7 @@ Proof.
   rewrite /bor /raw_bor /idx_bor /bor_idx. iSplit.
   - iDestruct 1 as (κ') "[? Hraw]". iDestruct "Hraw" as (s) "[??]".
     iExists (κ', s). by iFrame.
-  - iDestruct 1 as ([κ' s]) "[[??]?]".
-    iExists κ'. iFrame. iExists s. by iFrame.
+  - iDestruct 1 as ([κ' s]) "[[??]?]". iFrame.
 Qed.
 
 Lemma bor_iff κ P P' : ▷ □ (P ↔ P') -∗ &{κ}P -∗ &{κ}P'.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 47b7e97f4b812d39e58d4cfb87a7d6d0900ec6ee..8524692ac1d39d1b59810879360fefee645ff6ac 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -362,10 +362,9 @@ Section arc.
     (* Finish up the proof. *)
     iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lrc ◁ box (arc ty)]
         with "[] LFT HE Hna HL Hk [>-]"); last first.
-    { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
-      iSplitL "Hx↦"; first by iExists _; rewrite ->uninit_own; auto.
+    { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame "∗%".
       iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame. iLeft.
-      rewrite freeable_sz_full_S. iFrame. iExists _. by iFrame. }
+      rewrite freeable_sz_full_S. by iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
@@ -405,7 +404,7 @@ Section arc.
       iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame.
       iMod (create_weak (P1 ν) (P2 lrcbox ty.(ty_size))
             with "Hrcbox↦0 Hrcbox↦1 [-]") as (γ) "[Ha Htok]".
-      { rewrite freeable_sz_full_S. iFrame. iExists _. iFrame.
+      { rewrite freeable_sz_full_S. iFrame.
         by rewrite vec_to_list_length. }
       iExists γ, ν. iFrame. iSplitL; first by auto. iIntros "!>!>!> Hν".
       iDestruct (lft_tok_dead with "Hν H†") as "[]". }
@@ -894,7 +893,7 @@ Section arc.
       { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock.
         iFrame. iCombine "Hr1" "Hr2" as "Hr1". iCombine "Hr0" "Hr1" as "Hr".
         rewrite -[in _ +â‚— ty.(ty_size)]Hlen -heap_pointsto_vec_app
-                -heap_pointsto_vec_cons tctx_hasty_val' //. iFrame. iExists _. iFrame.
+                -heap_pointsto_vec_cons tctx_hasty_val' //. iFrame.
         iExists O, _, _. iSplit; first by auto. iFrame. iIntros "!> !% /=".
         rewrite app_length drop_length. lia. }
       iApply type_delete; [solve_typing..|].
diff --git a/theories/typing/lib/brandedvec.v b/theories/typing/lib/brandedvec.v
index 4cbc56fcc9de78bd094c9a04995cf45d2122b475..b793897422e71180035958dcffeeb5c30c34f659 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -130,12 +130,11 @@ Section brandedvec.
     iMod (frac_bor_acc with "LFT Hmem Hlft") as (q') "[>Hmt Hclose]"; first solve_ndisj.
     iDestruct "Hmt" as "[Hmt1 Hmt2]".
     iModIntro. iExists _.
-    iSplitL "Hmt1".
-    { iExists [_]. iNext. iFrame. iExists _. eauto with iFrame. }
+    iSplitL "Hmt1"; first by simpl; iFrame "∗#".
     iIntros "Htok2 Hmt1". iDestruct "Hmt1" as (vl') "[>Hmt1 #Hown']".
     iDestruct ("Htok" with "Htok2") as "$".
     iAssert (▷ ⌜1 = length vl'⌝)%I as ">%".
-    { iNext. iDestruct (ty_size_eq with "Hown'") as %->. done. }
+    { iNext. by iDestruct ("Hown'") as "[%x [Hown' ->]]". }
     destruct vl' as [|v' vl']; first done.
     destruct vl' as [|]; last first. { simpl in *. lia. }
     rewrite !heap_pointsto_vec_singleton.
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 3405077ee74781787d59a31269114efde0135fb8..2bf7a723865cd5342334be4d6ce1b33226a593fa 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -223,9 +223,7 @@ Section typing.
            [c ◁ box (&shr{α}(cell ty)); #x ◁ box (uninit ty.(ty_size)); #r ◁ box ty]
     with "[] LFT HE Htl HL HC"); last first.
     { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
-      iFrame "Hc". rewrite !tctx_hasty_val' //. iSplitL "Hx↦ Hx†".
-      - iFrame. iExists _. iFrame. iNext. iApply uninit_own. done.
-      - iFrame. iExists _. iFrame. }
+      iFrame "Hc". rewrite !tctx_hasty_val' //. iSplitL "Hx↦ Hx†"; by iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
diff --git a/theories/typing/lib/ghostcell.v b/theories/typing/lib/ghostcell.v
index 1cd696e9ec46a4984a1fbb867aa5439cf60d1534..62f928cb772eafaa5364bafc81a4a013068c87d1 100644
--- a/theories/typing/lib/ghostcell.v
+++ b/theories/typing/lib/ghostcell.v
@@ -143,9 +143,8 @@ Section ghostcell.
     iIntros (?????) "#Hκ H".
     iDestruct "H" as (γ) "[#? H]".
     iDestruct "H" as (κ'') "[? ?]".
-    iExists _. iFrame "#".
-    iExists κ''.
-    by iSplit; first iApply lft_incl_trans.
+    iFrame "∗#".
+    by iApply lft_incl_trans.
   Qed.
  
   Global Instance ghosttoken_wf α : TyWf (ghosttoken α) :=
@@ -431,10 +430,8 @@ Section ghostcell.
       iExists l, vl.
       iSplit; first done.
       simpl_subst.
-      iFrame.
-      iSplit; first by refine (match vl with Vector.nil => _ end).
-      iExists γ.
-      by iFrame "Hidx Hown".
+      iFrame "∗#".
+      by refine (match vl with Vector.nil => _ end).
     + iIntros (r) "Hna Hf Hown".
       simpl_subst.
       iDestruct ("Hcloseα" with "[Hf]") as "[Htok Hf]"; [by rewrite (right_id static)|].
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index e0830e404c098a6969865f883e08cd1b39f738bc..9b89451b816d9f2649a3cf227c7927bab8780b40 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -161,8 +161,8 @@ Section code.
         with "[] LFT HE Hna HL Hk"); last first.
     (* TODO: It would be nice to say [{#}] as the last spec pattern to clear the context in there. *)
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val' // tctx_hasty_val' //.
-      iFrame. iSplitL "Hx".
-      - iExists _. iFrame. by rewrite uninit_own vec_to_list_length.
+      iFrame. iSplitR.
+      - simpl. by rewrite vec_to_list_length.
       - iExists (#false :: vl). rewrite heap_pointsto_vec_cons. iFrame; eauto. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -199,10 +199,8 @@ Section code.
         with "[] LFT HE Hna HL Hk"); last first.
     (* TODO: It would be nice to say [{#}] as the last spec pattern to clear the context in there. *)
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val' // tctx_hasty_val' //.
-      iFrame. iSplitR "Hm0 Hm".
-      - iExists _. iFrame.
-      - iExists (_ :: _). rewrite heap_pointsto_vec_cons. iFrame.
-        rewrite uninit_own. rewrite /= vec_to_list_length. eauto. }
+      iFrame. iExists (_ :: _). rewrite heap_pointsto_vec_cons. iFrame.
+      rewrite uninit_own. rewrite /= vec_to_list_length. eauto. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index cc75fa98b3dbb126aa9b537b1ef2c2cc41b5473b..53e8bc63e4dea26b8b75a755b332b3c6827c40df 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -161,8 +161,7 @@ Section rc.
         { by apply auth_both_valid_discrete. }
         iMod (na_inv_alloc tid _ _ (rc_inv tid ν γ l' ty)
               with "[Ha Hν2 Hl'1 Hl'2 H† HPend]") as "#?".
-        { rewrite /rc_inv. iExists (Some $ Cinl (_, _), _). iFrame. iExists _.
-          iFrame "#∗". rewrite Qp.div_2; auto. }
+        { rewrite /rc_inv. iExists (Some $ Cinl (_, _), _). iFrame. rewrite Qp.div_2; auto. }
         iMod (ty_share with "LFT HP Hν1") as "[??]"; first solve_ndisj.
         iExists _, _, _. iFrame. iExists ty. iFrame "#". iSplitR; last by auto.
           by iApply type_incl_refl. }
@@ -375,7 +374,7 @@ Section code.
           { apply auth_update_dealloc.
             rewrite pair_op Cinl_op Some_op -{1}(left_id 0%nat _ weak) pair_op.
             apply (cancel_local_update_unit _ (_, _)). }
-          iApply "Hclose". iFrame. iExists _. iFrame. iExists (q+q'')%Qp. iFrame.
+          iApply "Hclose". iFrame. iExists _. iFrame "Hst". iExists (q+q'')%Qp. iFrame.
           iSplitL; first last.
           { rewrite [(_+_)%Qp]assoc [(q'+_)%Qp]comm. auto. }
           rewrite pos_op_add Z.sub_1_r -Pos2Z.inj_pred; last lia.
@@ -537,10 +536,9 @@ Section code.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lrc ◁ box (rc ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
-      iSplitL "Hx↦".
-      { iExists _. rewrite uninit_own. auto. }
+      iSplitR; first done.
       iNext. iExists [_]. rewrite heap_pointsto_vec_singleton. iFrame. iLeft.
-      rewrite freeable_sz_full_S. iFrame. iExists _. iFrame. }
+      rewrite freeable_sz_full_S. iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
@@ -1083,8 +1081,8 @@ Section code.
         iMod (bor_create _ ν with "LFT Hl3") as "[Hb Hh]"=>//. iExists _.
         iSplitR; first by iApply type_incl_refl.
         iMod (ty_share with "LFT Hb Hν1") as "[Hty Hν]"=>//.
-        iSplitR "Hty"; last by auto. iApply na_inv_alloc. iExists _. do 2 iFrame.
-        iExists _. iFrame. by rewrite Qp.div_2. }
+        iSplitR "Hty"; last by auto. iApply na_inv_alloc. iExists _. 
+        do 2 iFrame. by rewrite Qp.div_2. }
       iDestruct "Hty" as (ty') "#(Hty'ty & Hinv & Hs & Hν†)".
       iDestruct "Hs" as "[Hs|Hν']"; last by iDestruct (lft_tok_dead with "Hν Hν'") as "[]".
       wp_bind (of_val clone). iApply (wp_wand with "[Hna]").
@@ -1125,7 +1123,7 @@ Section code.
               with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite 3!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
                 !tctx_hasty_val' //. unlock. iFrame. iRight. iExists γ, ν, _.
-        unfold rc_persist, tc_opaque. iFrame "∗#". eauto. }
+        unfold rc_persist, tc_opaque. iFrame "∗#". }
       iApply type_letalloc_1; [solve_typing..|]. iIntros (rcold). simpl_subst.
       iApply type_let.
       { apply rc_drop_type. }
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 569e39ca82ea36b0c84e3579e6f71148c0e3c49f..4c688331b8bccd37ed2e673c69dde03d3eccac0d 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -406,12 +406,10 @@ Section code.
       destruct st as [[[q'' strong]| |]|]; [..|done|].
       - iExists _. iDestruct "Hrcst" as (q0) "(Hlw & >$ & Hrcst)". iRight.
         iSplitR; first by auto with lia. iIntros "!>?". iApply "Hclose". iFrame.
-        iExists _. iFrame. iExists _. iFrame.
-        by rewrite !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l.
+        iExists _. iFrame. by rewrite !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l.
       - iExists _. iDestruct "Hrcst" as "[Hlw >$]". iRight.
         iSplitR; first by auto with lia. iIntros "!>?". iApply "Hclose". iFrame.
-        iExists _. iFrame. simpl.
-        by rewrite !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l.
+        iExists _. iFrame. by rewrite !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l.
       - iExists _. iDestruct "Hrcst" as "(>Hlw & >$ & >H† & >H)". destruct weakc.
         + iLeft. iSplitR; first done. iMod ("Hclose" with "[$Hna Hrc●]") as "$".
           { iExists _. iFrame. }
@@ -475,7 +473,7 @@ Section code.
       iExists ty. iFrame "Hν†". iSplitR; first by iApply type_incl_refl.
       iSplitL; last by iRight. iMod (na_inv_alloc with "[-]") as "$"; last done.
       iExists _. iFrame. rewrite freeable_sz_full_S shift_loc_assoc. iFrame.
-      iExists _. iFrame. rewrite vec_to_list_length. auto. }
+      rewrite vec_to_list_length. auto. }
     iApply type_jump; solve_typing.
   Qed.
 End code.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 2c381d7cfbebd4df64b370099078387abf758351..c3402c9fdf48ab4e187aac7b55b5d501ed95a1c7 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -82,16 +82,14 @@ Section ref_functions.
     iIntros "[Hlr H↦]". wp_seq. iMod ("Hcloseα2" with "[$H◯] Hna") as "[Hα1 Hna]".
     iMod ("Hcloseδ" with "[H↦lrc H● Hν1 Hshr' H†] Hna") as "[Hδ Hna]".
     { iExists (Some (_, false, _, _)). rewrite Z.add_comm -Some_op -!pair_op agree_idemp.
-      iFrame. iExists _. iFrame.
-      rewrite (comm Qp.add) (assoc Qp.add) Qp.div_2 (comm Qp.add). auto. }
+      iFrame. rewrite (comm Qp.add) (assoc Qp.add) Qp.div_2 (comm Qp.add). auto. }
     iMod ("Hcloseβ" with "Hδ") as "Hβ". iMod ("Hcloseα1" with "[$H↦]") as "Hα2".
     iMod ("Hclose'" with "[$Hα1 $Hα2] HL") as "HL". iMod ("Hclose" with "Hβ HL") as "HL".
     iApply (type_type _ _ _
            [ x ◁ box (&shr{α}(ref β ty)); #lr ◁ box(ref β ty)]
         with "[] LFT HE Hna HL Hk"); first last.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-      rewrite /= freeable_sz_full. iFrame. iExists _. iFrame. simpl.
-      iExists _, _, _, _, _. iFrame "∗#". }
+      rewrite /= freeable_sz_full. iFrame "∗#". simpl. iFrame "∗#". }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
@@ -171,7 +169,7 @@ Section ref_functions.
         { apply auth_update_dealloc. rewrite -(right_id None op (Some _)).
           apply cancel_local_update_unit, _. }
         iApply "H†". replace 1%Qp with (q'+q'')%Qp by naive_solver. iFrame.
-      - simpl in *. setoid_subst. iExists (Some (ν, false, q0, n')). iFrame.
+      - simpl in *. setoid_subst. iExists (Some (ν, false, q0, n')). iFrame "Hshr H†".
         iAssert (lrc ↦ #(Z.pos n'))%I with "[H↦lrc]" as "$".
         { rewrite pos_op_add Z.sub_1_r -Pos2Z.inj_pred; last lia.
           by rewrite Pos.add_1_l Pos.pred_succ. }
@@ -350,8 +348,7 @@ Section ref_functions.
     rewrite !shift_loc_assoc. wp_write. do 3 (wp_op; wp_write).
     iMod ("Hclosena" with "[H↦lrc H● Hν1 Hshr' H†] Hna") as "[Hβ Hna]".
     { iExists (Some (_, false, _, _)). rewrite Z.add_comm -Some_op -!pair_op agree_idemp.
-      iFrame. iExists _. iFrame.
-      rewrite (comm Qp.add) (assoc Qp.add) Qp.div_2 (comm Qp.add). auto. }
+      iFrame. rewrite (comm Qp.add) (assoc Qp.add) Qp.div_2 (comm Qp.add). auto. }
     iMod ("Hβclose" with "Hβ") as "Hα". iMod ("Hclose1" with "Hα HL") as "HL".
     iApply (type_type _ [_] _ [ #lrefs ◁ box (Π[ref α ty1; ref α ty2]) ]
        with "[] LFT HE Hna HL Hk"); first last.
@@ -360,7 +357,7 @@ Section ref_functions.
       rewrite 3!heap_pointsto_vec_cons heap_pointsto_vec_singleton !shift_loc_assoc.
       iFrame. iExists [_;_], [_;_]. iSplit=>//=.
       iSplitL "Hν H◯"; [by auto 10 with iFrame|]. iExists [_;_], [].
-      iSplitR=>//=. rewrite right_id. auto 20 with iFrame. }
+      iSplitR=>//=. rewrite right_id. by iFrame "∗#". }
     iApply type_jump; solve_typing.
   Qed.
 End ref_functions.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 68237cf7293ab661b13644d065952dc9b36bd7f1..bff7a76bbf4c71ffbfee4fe58fd28116b3548c24 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -36,9 +36,8 @@ Section refcell_functions.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lr ◁ box (refcell ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=.
-      iFrame. iSplitL "Hx↦".
-      - iExists _. rewrite uninit_own. auto.
-      - simpl. iFrame. iExists (_::_). rewrite heap_pointsto_vec_cons. iFrame=>//=. }
+      iFrame. iSplitR; first done.
+      simpl. iFrame. iExists (_::_). rewrite heap_pointsto_vec_cons. by iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
@@ -70,10 +69,8 @@ Section refcell_functions.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit (S (ty_size ty))); #lr ◁ box ty]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
-      iSplitR "Hr↦ Hx".
-      - iExists (_::_). rewrite heap_pointsto_vec_cons uninit_own. iFrame.
-        rewrite /= vec_to_list_length. auto.
-      - iExists vl. iFrame. }
+      iExists (_::_). rewrite heap_pointsto_vec_cons uninit_own. iFrame.
+      by rewrite /= vec_to_list_length. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
@@ -109,8 +106,7 @@ Section refcell_functions.
     iApply (type_type _ _ _
             [ #lx ◁ box (uninit 1); #(lx' +ₗ 1) ◁ &uniq{α}ty]
             with "[] LFT HE Hna HL HC [-]"); last first.
-    { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
-      iNext. iExists _. rewrite uninit_own. iFrame. }
+    { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame. }
     iApply type_assign; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
@@ -189,7 +185,7 @@ Section refcell_functions.
             - done. }
           iFrame "∗#". iExists (Some (ν, false, _, _)). iFrame "∗#".
           rewrite [_ â‹… _]comm -Some_op -!pair_op agree_idemp. iFrame.
-          iExists _. iFrame. rewrite -(assoc Qp.add) Qp.div_2 //.
+          rewrite -(assoc Qp.add) Qp.div_2 //.
         - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]"; first done.
           iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
             auth_update_alloc, (op_local_update_discrete _ _ (reading_stR (1/2)%Qp ν)).
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index a5f24d8aba1498abf72b14e3794c1cad5bda255c..095a0f2641b9eedd5f020bf0e4be0d03a1ef4267 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -148,7 +148,7 @@ Section refmut_functions.
           apply (cancel_local_update_unit (writing_stR q _)), _. }
         iDestruct "INV" as "(H† & Hq & _)".
         rewrite /= (_:Z.neg (1%positive â‹… n') + 1 = Z.neg n');
-          last (rewrite pos_op_add; lia). iFrame.
+          last (rewrite pos_op_add; lia). iFrame "H↦lrc H†".
         iApply step_fupd_intro; [set_solver+|]. iSplitL; [|done].
         iDestruct "Hq" as (q' ?) "?". iExists (q+q')%Qp. iFrame.
         rewrite assoc (comm _ q'' q) //. }
@@ -325,7 +325,7 @@ Section refmut_functions.
     iMod ("Hclosena" with "[Hlrc H● Hν1 H†] Hna") as "[Hβ Hna]".
     { iExists (Some (_, true, _, _)).
       rewrite -Some_op -!pair_op agree_idemp /= (comm _ xH _).
-      iFrame. iSplitL; [|done]. iExists _. iFrame.
+      iFrame.
       rewrite (comm Qp.add) (assoc Qp.add) Qp.div_2 (comm Qp.add). auto. }
     iMod ("Hβclose" with "Hβ") as "Hα". iMod ("Hclose1" with "Hα HL") as "HL".
     iApply (type_type _ [_] _ [ #lrefmuts ◁ box (Π[refmut α ty1; refmut α ty2]) ]
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index f3038b00d7082c6d4718dc3901f31f0b7d21a64f..bd42d400612f5b40017221ffc5f7947c113df770 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -38,9 +38,8 @@ Section rwlock_functions.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lr ◁ box (rwlock ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
-      iSplitL "Hx↦".
-      - iExists _. rewrite uninit_own. auto.
-      - iExists (_::_). rewrite heap_pointsto_vec_cons. iFrame. simpl. iFrame. auto. }
+      iSplitR; first done.
+      iExists (_::_). rewrite heap_pointsto_vec_cons. iFrame. simpl. iFrame. auto. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
@@ -73,9 +72,7 @@ Section rwlock_functions.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit (S (ty_size ty))); #lr ◁ box ty]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
-      iSplitR "Hr↦ Hx".
-      - iExists (_::_). rewrite heap_pointsto_vec_cons uninit_own -Hsz. iFrame. auto.
-      - iExists vl. iFrame. }
+      iExists (_::_). rewrite heap_pointsto_vec_cons uninit_own -Hsz. iFrame. auto. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
@@ -109,8 +106,7 @@ Section rwlock_functions.
     iApply (type_type _ _ _
             [ #lx ◁ box (uninit 1); #(lx' +ₗ 1) ◁ &uniq{α}ty]
             with "[] LFT HE Hna HL HC [-]"); last first.
-    { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
-      iNext. iExists _. rewrite uninit_own. iFrame. }
+    { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame. }
     iApply type_assign; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index 3c51bb4377a3d94be21fe9201959378567974cd0..833d6fb42b41a8b665ece311e2e808d694d04638 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -44,7 +44,7 @@ Section code.
     iApply (type_call_iris _ [ϝ] () [_; _]
       with "LFT HE Hna [Hϝ] Hf' [Henv Htl Htl† Hx'vl]"); [solve_typing| | |].
     { by rewrite /= (right_id static). }
-    { rewrite /= !tctx_hasty_val tctx_hasty_val' //. iFrame. iExists _. iFrame. }
+    { rewrite /= !tctx_hasty_val tctx_hasty_val' //. iFrame. }
     (* Prove the continuation of the function call. *)
     iIntros (r) "Hna Hϝ Hr". simpl.
     iDestruct (ownptr_own with "Hr") as (lr rvl) "(% & Hlr & Hrvl & Hlr†)". subst r.
@@ -60,7 +60,7 @@ Section code.
     iApply (type_type _ _ _ [ x ◁ _; #lr ◁ box (uninit ty.(ty_size)) ]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame. iExists _. rewrite uninit_own. iFrame. auto using vec_to_list_length. }
+      unlock. iFrame. auto using vec_to_list_length. }
     iApply type_delete; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
     iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 0c315e44cef0434e5c919eb8c920ab36f75f7543..0e85a682e283b037267b84bf95510a2494c66cb6 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -196,8 +196,7 @@ Section util.
     - iIntros "Hown". destruct v as [[|l|]|]; try done.
       iExists l. iDestruct "Hown" as "[Hown $]". rewrite heap_pointsto_ty_own.
       iDestruct "Hown" as (vl) "[??]". eauto with iFrame.
-    - iIntros "Hown". iDestruct "Hown" as (l vl) "(% & ? & ? & ?)". subst v.
-      iFrame. iExists _. iFrame.
+    - iIntros "Hown". iDestruct "Hown" as (l vl) "(% & ? & ? & ?)". subst v. iFrame.
   Qed.
 
   Lemma ownptr_uninit_own n m tid v :
@@ -225,7 +224,7 @@ Section typing.
     rewrite typed_write_eq. iIntros (Hsz) "!>".
     iIntros ([[]|] tid F qmax qL ?) "_ _ $ Hown"; try done.
     rewrite /= Hsz. iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
-    iDestruct (ty_size_eq with "Hown") as "#>%". iExists _, _. iFrame "H↦". auto.
+    iDestruct (ty_size_eq with "Hown") as "#>%". iFrame. auto.
   Qed.
 
   Lemma read_own_copy E L ty n :
@@ -233,9 +232,9 @@ Section typing.
   Proof.
     rewrite typed_read_eq. iIntros (Hsz) "!>".
     iIntros ([[|l|]|] tid F qmax qL ?) "_ _ $ $ Hown"; try done.
-    iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ #Hown]".
-    iExists l, _, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !>".
-    iExists _. auto.
+    iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ #Hown]".
+    iExists l, _, _. iSplitR; first done. 
+    unfold heap_pointsto_vec at 1. iSplitL; iFrame "∗#"; auto.
   Qed.
 
   Lemma read_own_move E L ty n :
@@ -243,10 +242,11 @@ Section typing.
   Proof.
     rewrite typed_read_eq. iModIntro.
     iIntros ([[|l|]|] tid F qmax qL ?) "_ _ $ $ Hown"; try done.
-    iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
+    iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
     iDestruct (ty_size_eq with "Hown") as "#>%".
-    iExists l, vl, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !> !>".
-    iExists _. iFrame. done.
+    iExists l, vl, _. iSplitR; first done. 
+    unfold heap_pointsto_vec. iSplitL "H↦"; iFrame "∗#"; auto.
+    by iIntros "!> $".
   Qed.
 
   Lemma type_new_instr {E L} (n : Z) :
@@ -257,8 +257,7 @@ Section typing.
     iIntros (? tid qmax) "#LFT #HE $ $ _".
     iApply wp_new; try done. iModIntro.
     iIntros (l) "(H† & Hlft)". rewrite tctx_interp_singleton tctx_hasty_val.
-    iNext. rewrite freeable_sz_full Z2Nat.id //. iFrame.
-    iExists (repeat #☠ (Z.to_nat n)). iFrame. by rewrite /= repeat_length.
+    iNext. rewrite freeable_sz_full Z2Nat.id //. iFrame. by rewrite /= repeat_length.
   Qed.
 
   Lemma type_new {E L C T} (n' : nat) x (n : Z) e :
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 7d4bf78f23291f13fc3ec19f526c430baa3af303..fe940a21d80157abd1b8b634ebc53eaa25fca1df 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -44,7 +44,7 @@ Section product.
     - iDestruct "H" as "[H1 H2]". iDestruct "H1" as (vl1) "[H↦1 H1]".
       iDestruct "H2" as (vl2) "[H↦2 H2]". iExists (vl1 ++ vl2).
       rewrite heap_pointsto_vec_app. iDestruct (ty_size_eq with "H1") as %->.
-      iFrame. iExists _, _. by iFrame.
+      by iFrame.
   Qed.
 
   Program Definition product2 (ty1 ty2 : type) :=
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index b652d36f65b191b0e995cd5bdc779e39fd20a6de..a545e55593b1594ba82a46b62706aec052173081 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -96,9 +96,9 @@ Section product_split.
     iDestruct "H†" as "[H†1 H†2]". iDestruct "H↦" as "[H↦1 H↦2]".
     iDestruct (ty_size_eq with "H1") as "#>EQ".
     iDestruct "EQ" as %->. iSplitL "H↦1 H†1 H1".
-    + iExists _. iFrame "#∗". iExists _. by iFrame.
+    + iExists _. by iFrame "#∗".
     + iExists _. iSplitR; first (by simpl; iDestruct "Hp" as %->).
-      iFrame. iExists _. by iFrame.
+      by iFrame.
   Qed.
 
   Lemma tctx_merge_own_prod2 E L p n ty1 ty2 :
@@ -113,9 +113,8 @@ Section product_split.
     rewrite Hρ1. iDestruct "Hp2" as %[=<-]. iDestruct "H2" as "[H↦2 H†2]".
     iExists #l. iSplitR; first done. rewrite /= -freeable_sz_split. iFrame.
     iDestruct "H↦1" as (vl1) "[H↦1 H1]". iDestruct "H↦2" as (vl2) "[H↦2 H2]".
-    iExists (vl1 ++ vl2). rewrite heap_pointsto_vec_app. iFrame.
-    iDestruct (ty_size_eq with "H1") as "#>EQ". iDestruct "EQ" as %->.
-    rewrite {3}/ty_own /=. auto 10 with iFrame.
+    iExists (vl1 ++ vl2). rewrite heap_pointsto_vec_app.
+    iDestruct (ty_size_eq with "H1") as "#>->". by iFrame.
   Qed.
 
   Lemma tctx_split_own_prod E L n tyl p :
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 17b45d45078f838259e19c74abcc191adec9ed35..2d8fb4de5ab669b851fd9b4ee617bc0053f90e32 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -48,7 +48,7 @@ Section sum.
       iDestruct (ty_size_eq with "Hown") as "#EQ". iDestruct "EQ" as %Hvl'.
       iExists (#i::vl'++vl'').
       rewrite heap_pointsto_vec_cons heap_pointsto_vec_app (shift_loc_assoc_nat _ 1) Hvl'.
-      iFrame. iExists i, vl', vl''. iSplit; first done. iFrame. iPureIntro.
+      iFrame. iExists vl''. iSplit; first done. iPureIntro.
       simpl. f_equal. by rewrite app_length Hvl'.
   Qed.
 
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 1ccdfae180671778998b808f411c7a049fae5f09..c1efe2657b0f0c0ab013111e90f511cf76febbe8 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -39,7 +39,7 @@ Section case.
         iFrame. auto.
       + eauto with iFrame.
       + rewrite -EQlen app_length Nat.add_comm Nat.add_sub shift_loc_assoc_nat.
-        iFrame. iExists _. iFrame. auto.
+        by iFrame.
     - rewrite /= -EQlen app_length -(Nat.add_1_l (_+_)) -!freeable_sz_split. iFrame.
       iExists (#i :: vl' ++ vl''). iNext. rewrite heap_pointsto_vec_cons heap_pointsto_vec_app.
       iFrame. iExists i, vl', vl''. rewrite /= app_length nth_lookup EQty /=. auto.
@@ -265,10 +265,8 @@ Section case.
     { iApply "HLclose". by iFrame. }
     iNext.
     rewrite split_sum_mt /is_pad. iExists i. rewrite nth_lookup Hty. iFrame.
-    iSplitL "H↦pad".
-    - rewrite (shift_loc_assoc_nat _ 1) take_length Nat.min_l; last lia.
-      iExists _. iFrame. rewrite /= drop_length. iPureIntro. lia.
-    - iExists _. iFrame.
+    rewrite (shift_loc_assoc_nat _ 1) take_length Nat.min_l; last lia. iFrame.
+    rewrite /= drop_length. iPureIntro. lia.
   Qed.
 
   Lemma type_sum_memcpy {E L} sty tyl i ty1 ty2 ty n ty1' ty2' C T T' p1 p2 e: