diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index e6111801d1d9b3b4ce856412a32fdf36fccb5fd9..c50a56d4d76870d04804b2681f83cddeb88e5644 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -407,7 +407,7 @@ Section arc.
             split; last by rewrite /= left_id; apply Hv. split=>[|//].
             apply frac_valid. rewrite /= -Heq comm_L.
             by apply Qp.add_le_mono_l, Qp.div_le. }
-          iFrame. iApply "Hclose1". iExists _. iFrame. iExists _. iFrame.
+          iFrame. iApply "Hclose1". iExists _. iFrame.
           rewrite /= [xH â‹… _]comm_L frac_op [(_ + q')%Qp]comm -[(_ + _)%Qp]assoc
                   Qp.div_2 left_id_L. auto with iFrame.
         + iIntros "Hl". iFrame. iApply ("Hclose1" with "[-]"). iExists _. iFrame.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 8524692ac1d39d1b59810879360fefee645ff6ac..4712bfc6821985103be57730f655b98d21d60da3 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -792,8 +792,8 @@ Section arc.
     (* Finish up the proof. *)
     iApply (type_type _ _ _ [ rcx ◁ box (uninit 1); r ◁ box (option ty) ]
             with "[] LFT HE Hna HL Hk [-]"); last first.
-    { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock. iFrame.
-      by rewrite tctx_hasty_val. }
+    { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock.
+      rewrite tctx_hasty_val. iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
@@ -827,8 +827,8 @@ Section arc.
     (* Finish up the proof. *)
     iApply (type_type _ _ _ [ rcx ◁ box (uninit 1); r ◁ box (uninit 0) ]
             with "[] LFT HE Hna HL Hk [-]"); last first.
-    { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock. iFrame.
-      by rewrite tctx_hasty_val. }
+    { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val. unlock.
+      rewrite tctx_hasty_val. iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
diff --git a/theories/typing/lib/brandedvec.v b/theories/typing/lib/brandedvec.v
index b793897422e71180035958dcffeeb5c30c34f659..ce5730cb6b0fe77b18aa5ca06231c4162e2348e8 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -200,10 +200,7 @@ Section typing.
       iSplitR; first done.
       simpl.
       rewrite freeable_sz_full.
-      iFrame.
-      iExists 0%nat.
-      iSplitL; last done.
-      iExists γ; iSplitR; by eauto. }
+      by iFrame "#∗". }
     iMod ("Hn'" with "[%]") as (α) "[Hn Htok]"; [solve_typing..|].
     wp_let.
     iMod (lctx_lft_alive_tok ϝ with "HE HL")
@@ -398,11 +395,7 @@ Section typing.
     iMod ("Hclose'" with "[H↦ Hidx Hown]") as "[Hn Hβ]".
     { iExists (#(n+1)::nil).
       rewrite heap_pointsto_vec_singleton.
-      iFrame "∗".
-      iIntros "!>".
-      iExists (n + 1)%nat.
-      iSplitL; last by (iPureIntro; do 3 f_equal; lia).
-      iExists γ. eauto with iFrame.
+      iFrame "#∗". iPureIntro; do 3 f_equal; lia.
     }
     iMod ("Hclose" with "Hβ HL") as "HL".
     iApply (type_type _ _ _ [ r ◁ box (uninit 1); #n ◁ brandidx _]
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 53e8bc63e4dea26b8b75a755b332b3c6827c40df..f2af7f3adbbe63efbc6f38b3081ed95f670943fb 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -321,8 +321,8 @@ Section code.
                 iSplitL "Hty".
                 { iDestruct "Hty" as (vy) "[H Hty]". iExists vy. iFrame.
                   by iApply "Hinclo". }
-                iIntros "!> H". iApply ("Hclose" with "[>-]"). iFrame. iExists _.
-                iFrame. rewrite Hincls /= !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l.
+                iIntros "!> H". iApply ("Hclose" with "[>-]"). iFrame.
+                rewrite Hincls /= !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l.
                 by iFrame.
         * iIntros "Hl1".
           iMod (own_update_2 with "Hst Htok") as "[Hst Htok]".
@@ -374,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 "Hst". iExists (q+q'')%Qp. iFrame.
+          iApply "Hclose". iFrame "Hst Hl2 Hl† Hna Hν†". 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.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 4c688331b8bccd37ed2e673c69dde03d3eccac0d..9a1c5996bc3c1b9faa9291e5693f500509615598 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -406,16 +406,16 @@ 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. by rewrite !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l.
+        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. by rewrite !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l.
+        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. }
           rewrite Hszeq. auto with iFrame.
         + iRight. iSplitR; first by auto with lia. iIntros "!>?". iApply "Hclose".
-          iFrame. iExists _. iFrame.
+          iFrame.
           by rewrite !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l. }
     - subst. wp_read. wp_let. wp_op. wp_if.
       iApply (type_type _ _ _ [ w ◁ box (uninit 1); #lw ◁ box (uninit (2 + ty.(ty_size))) ]
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 24bb58414b436d9414e4fd7c00fbfa8b5385e1da..9676e30c513b4d7f8af158d956829c7348ab7b14 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -164,7 +164,7 @@ Section rwlock.
       rewrite Qp.div_2.  iSplitL; last by auto.
       iIntros "!> !> Hν". iDestruct (lft_tok_dead with "Htok Hν") as "[]".
     - iMod (own_alloc (● writing_st)) as (γ) "Hst". { by apply auth_auth_valid. }
-      iFrame. iExists _, _. eauto with iFrame.
+      by iFrame.
   Qed.
   Next Obligation.
     iIntros (?????) "#Hκ H". iDestruct "H" as (α γ) "[#??]".
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index bd42d400612f5b40017221ffc5f7947c113df770..9e7068bb34612c66adc1a67981681729612a99f2 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -192,8 +192,8 @@ Section rwlock_functions.
               - apply frac_valid. rewrite /= -Hqq' comm_L.
                 by apply Qp.add_le_mono_l, Qp.div_le.
               - done. }
-            iFrame "∗#". iExists _. rewrite Z.add_comm /=. iFrame. iExists _, _.
-            iFrame "∗#". iSplitR; first by rewrite /= Hag agree_idemp.
+            iFrame "∗#". rewrite Z.add_comm /=. iFrame.
+            iSplitR; first by rewrite /= Hag agree_idemp.
             rewrite (comm Qp.add) (assoc Qp.add) Qp.div_2 (comm Qp.add). auto.
           - iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]"; first solve_ndisj.
             iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
@@ -215,8 +215,8 @@ Section rwlock_functions.
                      #lx ◁ rwlockreadguard α ty]
               with "[] LFT HE Hna HL Hk"); first last.
         { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
-                  tctx_hasty_val' //. iFrame.
-          iExists _, _, _, _, _. iFrame "∗#". iApply ty_shr_mono; last done.
+                  tctx_hasty_val' //. iFrame "∗#".
+          iApply ty_shr_mono; last done.
           iApply lft_intersect_mono; first done. iApply lft_incl_refl. }
         iApply (type_sum_assign (option $ rwlockreadguard α ty)); [solve_typing..|].
         simpl. iApply type_jump; solve_typing.
@@ -290,7 +290,7 @@ Section rwlock_functions.
                      #lx ◁ rwlockwriteguard α ty]
               with "[] LFT HE Hna HL Hk"); first last.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
-                tctx_hasty_val' //. iFrame. iExists _, _, _. iFrame "∗#". }
+                tctx_hasty_val' //. iFrame "∗#". }
       iApply (type_sum_assign (option $ rwlockwriteguard α ty)); [solve_typing..|].
       simpl. iApply type_jump; solve_typing.
   Qed.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index fe940a21d80157abd1b8b634ebc53eaa25fca1df..f647f477746ea2c11eed783e167fd01f6b174cc7 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -201,10 +201,10 @@ Section typing.
     iSplit; first by rewrite /= assoc. iSplit; iIntros "!> *"; iSplit; iIntros "H".
     - iDestruct "H" as (vl1 vl') "(% & Ho1 & H)".
       iDestruct "H" as (vl2 vl3) "(% & Ho2 & Ho3)". subst.
-      iExists _, _. iSplit; first by rewrite assoc. iFrame. iExists _, _. by iFrame.
+      iExists _, _. iSplit; first by rewrite assoc. by iFrame.
     - iDestruct "H" as (vl1 vl') "(% & H & Ho3)".
       iDestruct "H" as (vl2 vl3) "(% & Ho1 & Ho2)". subst.
-      iExists _, _. iSplit; first by rewrite -assoc. iFrame. iExists _, _. by iFrame.
+      iExists _, _. iSplit; first by rewrite -assoc. by iFrame.
     - iDestruct "H" as "(Hs1 & Hs2 & Hs3)". rewrite shift_loc_assoc_nat.
       by iFrame.
     - iDestruct "H" as "[[Hs1 Hs2] Hs3]". rewrite /= shift_loc_assoc_nat.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index a545e55593b1594ba82a46b62706aec052173081..f575e1aa0987b0eb8631c3cc253f635b5ba5bd8e 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -78,8 +78,7 @@ Section product_split.
       rewrite Nat.add_comm -hasty_ptr_offsets_offset //. }
     iClear "IH". iMod (Hmerge with "LFT HE HL [Hty Htyl]") as "($ & ?)";
                    last by rewrite tctx_interp_singleton.
-    rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton. iFrame.
-    iExists #l. iSplit; done.
+    rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton. by iFrame.
   Qed.
 
   (** Owned pointers *)