diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index a51c6ba362c8b3d35a5fd530524168a4ee39836b..9f8287886c684a5c1b2b5d17bb6d8725e5961cb9 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -20,7 +20,7 @@ Section typing.
   Lemma type_bool (b : Datatypes.bool) E L :
     typed_instruction_ty E L [] #b bool.
   Proof.
-    iIntros (tid qE) "_ _ $ $ $ _". wp_value.
+    iAlways. iIntros (tid qE) "_ _ $ $ $ _". wp_value.
     rewrite tctx_interp_singleton tctx_hasty_val. iExists _. done.
   Qed.
 
@@ -29,7 +29,7 @@ Section typing.
     typed_body E L C T e1 → typed_body E L C T e2 →
     typed_body E L C T (if: p then e1 else e2).
   Proof.
-    iIntros (Hp He1 He2 tid qE) "#HEAP #LFT Htl HE HL HC HT".
+    iIntros (Hp He1 He2) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT".
     iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "#Hp".
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
     iDestruct "Hown" as (b) "Hv". iDestruct "Hv" as %[=->].
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 64aff4a2ac21274319b28c395151a8f45e7c542e..13baa93ed15529a043fba24ad74af5cfd99bf174 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -44,7 +44,7 @@ Section borrow.
     lctx_lft_alive E L κ →
     typed_instruction_ty E L [p ◁ &uniq{κ} own n ty] (!p) (&uniq{κ} ty).
   Proof.
-    iIntros (Hκ tid eq) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
+    iIntros (Hκ) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
     iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
     iDestruct "Hown" as (l P) "[[Heq #HPiff] HP]". iDestruct "Heq" as %[=->].
@@ -67,7 +67,7 @@ Section borrow.
     lctx_lft_alive E L κ →
     typed_instruction_ty E L [p ◁ &shr{κ} own n ty] (!p) (&shr{κ} ty).
   Proof.
-    iIntros (Hκ tid eq) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
+    iIntros (Hκ) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
     iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
     iDestruct "Hown" as (l) "[Heq #H↦]". iDestruct "Heq" as %[=->].
@@ -84,7 +84,7 @@ Section borrow.
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
     typed_instruction_ty E L [p ◁ &uniq{κ} &uniq{κ'} ty] (!p) (&uniq{κ} ty).
   Proof.
-    iIntros (Hκ Hincl tid eq) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
+    iIntros (Hκ Hincl) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
     iPoseProof (Hincl with "[#] [#]") as "Hincl".
     { by iApply elctx_interp_persist. } { by iApply llctx_interp_persist. }
     iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
@@ -114,7 +114,7 @@ Section borrow.
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
     typed_instruction_ty E L [p ◁ &shr{κ} &uniq{κ'} ty] (!p) (&shr{κ} ty).
   Proof.
-    iIntros (Hκ Hincl tid eq) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
+    iIntros (Hκ Hincl) "!# * #HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
     iPoseProof (Hincl with "[#] [#]") as "Hincl".
     { by iApply elctx_interp_persist. } { by iApply llctx_interp_persist. }
     iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 99e45babef51794390b62c7d7d0d8cb942f458cc..10926c2f8485acd1a98c234859c513949c9498af 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -13,7 +13,7 @@ Section typing.
     tctx_incl E L T (T' (list_to_vec args)) →
     typed_body E L C T (k (of_val <$> args)).
   Proof.
-    iIntros (HC Hincl tid qE) "#HEAP #LFT Htl HE HL HC HT".
+    iIntros (HC Hincl) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT".
     iMod (Hincl with "LFT HE HL HT") as "(HE & HL & HT)".
     iSpecialize ("HC" with "HE * []"); first done.
     rewrite -{3}(vec_to_list_of_list args). iApply ("HC" with "* Htl HL HT").
@@ -26,7 +26,7 @@ Section typing.
     (∀ k, typed_body E L2 (k ◁cont(L1, T') :: C) T (subst' kb k e2)) →
     typed_body E L2 C T (letcont: kb argsb := econt in e2).
   Proof.
-    iIntros (Hc1 Hc2 Hecont He2 tid qE) "#HEAP #LFT Htl HE HL HC HT". iApply wp_let'.
+    iIntros (Hc1 Hc2 Hecont He2) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT". iApply wp_let'.
     { simpl. rewrite decide_left. done. }
     iModIntro. iApply (He2 with "* HEAP LFT Htl HE HL [HC] HT"). clear He2.
     iIntros "HE". iLöb as "IH". iIntros (x) "H".
diff --git a/theories/typing/function.v b/theories/typing/function.v
index ac9c37cbed279b54c8335cf2de84ca033ce6435b..a3e30cdcfdfe0d6d3ee06ffe9e9f5e238da61b84 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -12,7 +12,7 @@ Section fn.
           (tys : A → vec type n) (ty : A → type) : type :=
     {| st_own tid vl := (∃ fb kb xb e H,
          ⌜vl = [@RecV fb (kb::xb) e H]⌝ ∗ ⌜length xb = n⌝ ∗
-         □ ▷ ∀ (x : A) (k : val) (xl : vec val (length xb)),
+         ▷ ∀ (x : A) (k : val) (xl : vec val (length xb)),
             typed_body (E x) []
                        [k◁cont([], λ v : vec _ 1, [v!!!0 ◁ ty x])]
                        (zip_with (TCtx_hasty ∘ of_val) xl (tys x))
@@ -30,7 +30,7 @@ Section fn.
   Proof.
     intros ?? Htys ?? Hty. unfold fn. f_equiv. rewrite st_dist_unfold /=.
     f_contractive=>tid vl. unfold typed_body.
-    do 13 f_equiv. f_contractive. do 17 f_equiv.
+    do 12 f_equiv. f_contractive. do 18 f_equiv.
     - rewrite !cctx_interp_singleton /=. do 5 f_equiv.
       rewrite !tctx_interp_singleton /tctx_elt_interp. do 3 f_equiv. apply Hty.
     - rewrite /tctx_interp !big_sepL_zip_with /=. do 3 f_equiv.
@@ -72,8 +72,8 @@ Section typing.
   Proof.
     intros HE Htys Hty. apply subtype_simple_type=>//= _ vl.
     iIntros "#LFT #HE0 #HL0 Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
-    iExists fb, kb, xb, e, _. iSplit. done. iSplit. done. iAlways. iNext.
-    rewrite /typed_body. iIntros "* #HEAP _ Htl HE HL HC HT".
+    iExists fb, kb, xb, e, _. iSplit. done. iSplit. done. iNext.
+    rewrite /typed_body. iIntros "* !# * #HEAP _ Htl HE HL HC HT".
     iDestruct (elctx_interp_persist with "HE") as "#HEp".
     iMod (HE with "HE0 HL0 * HE") as (qE') "[HE' Hclose]". done.
     iApply ("Hf" with "* HEAP LFT Htl HE' HL [HC Hclose] [HT]").
@@ -152,7 +152,7 @@ Section typing.
     apply subtype_simple_type=>//= _ vl.
     iIntros "#LFT _ _ Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
     iExists fb, kb, xb, e, _. iSplit. done. iSplit. done.
-    rewrite /typed_body. iAlways. iNext. iIntros "*". iApply "Hf".
+    rewrite /typed_body. iNext. iIntros "*". iApply "Hf".
   Qed.
 
   (* TODO: Define some syntactic sugar for calling and letrec like we do on paper. *)
@@ -163,7 +163,7 @@ Section typing.
                ((p ◁ fn E' tys ty) :: zip_with TCtx_hasty ps (tys x) ++ T)
                (call: p ps → k).
   Proof.
-    iIntros (HE tid qE) "#HEAP #LFT Htl HE HL HC".
+    iIntros (HE) "!# * #HEAP #LFT Htl HE HL HC".
     rewrite tctx_interp_cons tctx_interp_app. iIntros "(Hf & Hargs & HT)".
     wp_bind p. iApply (wp_hasty with "Hf"). iIntros (v) "% Hf".
     iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = k⌝):::
@@ -255,12 +255,12 @@ Section typing.
                    (subst_v (fb :: kb :: argsb) (f ::: k ::: args) e)) →
     typed_instruction_ty E L T (funrec: fb argsb → kb := e) (fn E' tys ty).
   Proof.
-    iIntros (Hc Hbody tid qE) "#HEAP #LFT $ $ $ #HT". iApply wp_value.
+    iIntros (Hc Hbody) "!# * #HEAP #LFT $ $ $ #HT". iApply wp_value.
     { simpl. rewrite decide_left. done. }
     rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
     { simpl. rewrite decide_left. done. }
-    iExists fb, kb, argsb, e, _. iSplit. done. iSplit. done. iAlways. iNext. clear qE.
-    iIntros (x k args tid' qE) "_ _ Htl HE HL HC HT'".
+    iExists fb, kb, argsb, e, _. iSplit. done. iSplit. done. iNext. clear qE.
+    iIntros (x k args) "!#". iIntros (tid' qE) "_ _ Htl HE HL HC HT'".
     iApply (Hbody with "* HEAP LFT Htl HE HL HC").
     rewrite tctx_interp_cons tctx_interp_app. iFrame "HT' IH".
     by iApply sendc_change_tid.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 1da981dfe92974c2f0104fe245add2af5ab48fba..5b4cc7e398f50ead1853c3f83f69cfba14db0607 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -19,14 +19,14 @@ Section typing.
   Lemma type_int (z : Z) E L :
     typed_instruction_ty E L [] #z int.
   Proof.
-    iIntros (tid qE) "_ _ $ $ $ _". wp_value.
+    iAlways. iIntros (tid qE) "_ _ $ $ $ _". wp_value.
     rewrite tctx_interp_singleton tctx_hasty_val. iExists _. done.
   Qed.
 
   Lemma type_plus E L p1 p2 :
     typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 + p2) int.
   Proof.
-    iIntros (tid qE) "_ _ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
+    iAlways. iIntros (tid qE) "_ _ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
     iIntros "[Hp1 Hp2]".
     wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "_ Hown1".
     wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "_ Hown2".
@@ -39,7 +39,7 @@ Section typing.
   Lemma type_minus E L p1 p2 :
     typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 - p2) int.
   Proof.
-    iIntros (tid qE) "_ _ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
+    iAlways. iIntros (tid qE) "_ _ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
     iIntros "[Hp1 Hp2]".
     wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "_ Hown1".
     wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "_ Hown2".
@@ -52,7 +52,7 @@ Section typing.
   Lemma type_le E L p1 p2 :
     typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 ≤ p2) bool.
   Proof.
-    iIntros (tid qE) "_ _ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
+    iAlways. iIntros (tid qE) "_ _ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
     iIntros "[Hp1 Hp2]".
     wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "_ Hown1".
     wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "_ Hown2".
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 9bbd80cb58c57454ce1b65744c6e2cf405788e1e..393c71b8a98c70972131477e5770f5ee515127a1 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -158,7 +158,7 @@ Section typing.
   Lemma write_own {E L} ty ty' n :
     ty.(ty_size) = ty'.(ty_size) → typed_write E L (own n ty') ty (own n ty).
   Proof.
-    iIntros (Hsz p tid F qE qL ?) "_ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
+    iIntros (Hsz) "!#". iIntros (p tid F qE qL ?) "_ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
     iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
     (* This turns out to be the fastest way to apply a lemma below â–· -- at
     least if we're fine throwing away the premise even though the result
@@ -172,7 +172,7 @@ Section typing.
   Lemma read_own_copy E L ty n :
     Copy ty → typed_read E L (own n ty) ty (own n ty).
   Proof.
-    iIntros (Hsz p tid F qE qL ?) "_ $ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
+    iIntros (Hsz) "!#". iIntros (p tid F qE qL ?) "_ $ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
     iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ #Hown]". iModIntro.
     iExists l, _, _. iSplit; first done. iFrame "∗#". iIntros "Hl !>".
     iExists _. iSplit; first done. iFrame "H†". iExists _. by iFrame.
@@ -181,7 +181,7 @@ Section typing.
   Lemma read_own_move E L ty n :
     typed_read E L (own n ty) ty (own n $ uninit ty.(ty_size)).
   Proof.
-    iIntros (p tid F qE qL ?) "_ $ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
+    iAlways. iIntros (p tid F qE qL ?) "_ $ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
     iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
     iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">%".
     { by iApply ty_size_eq. }
@@ -193,7 +193,7 @@ Section typing.
   Lemma type_new {E L} (n : nat) :
     typed_instruction_ty E L [] (new [ #n ]%E) (own n (uninit n)).
   Proof.
-    iIntros (tid eq) "#HEAP #LFT $ $ $ _".
+    iAlways. iIntros (tid eq) "#HEAP #LFT $ $ $ _".
     iApply (wp_new with "HEAP"); try done; first omega. iModIntro.
     iIntros (l vl) "(% & H† & Hlft)". rewrite tctx_interp_singleton tctx_hasty_val.
     iExists _. iSplit; first done. iNext. rewrite Nat2Z.id freeable_sz_full. iFrame.
@@ -208,7 +208,7 @@ Section typing.
     ty.(ty_size) = n →
     typed_instruction E L [p ◁ own n ty] (delete [ #n; p])%E (λ _, []).
   Proof.
-    iIntros (<- tid eq) "#HEAP #LFT $ $ $ Hp". rewrite tctx_interp_singleton.
+    iIntros (<-) "!#". iIntros (tid eq) "#HEAP #LFT $ $ $ Hp". rewrite tctx_interp_singleton.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
     iDestruct "Hown" as (l) "(Hv & H↦∗: & >H†)". iDestruct "Hv" as %[=->].
     iDestruct "H↦∗:" as (vl) "[>H↦ Hown]". rewrite tctx_interp_nil.
@@ -264,7 +264,12 @@ Section typing.
         - eapply is_closed_subst. done. set_solver. }
       eapply type_let'.
       + apply subst_is_closed; last done. apply is_closed_of_val.
-      + eapply type_memcpy; try done. by eapply (write_own _ (uninit _)).
+      + eapply type_memcpy; first done; last done.
+        (* TODO: Doing "eassumption" here shows that unification takes *forever* to fail.
+           I guess that's caused by it trying to unify typed_read and typed_write,
+           but considering that the Iris connectives are all sealed, why does
+           that take so long? *)
+        by eapply (write_own _ (uninit _)).
       + solve_typing.
       + move=>//=.
   Qed.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 1214d2f4edfda430ea7cb07167874b7fc29540b1..98e46c54169f43dd3cdcae7b304632c2aca1b1c7 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -220,7 +220,10 @@ Section typing_rules.
                       (λ _, [p1 ◁ ty1'; p2 ◁ ty2']%TC).
   Proof.
     iIntros (Hsz Hwrt Hread) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HT".
-    iApply (type_memcpy_iris with "* [] [] []"). [$HEAP $LFT $Htl $HE $HL HT]"). ; try done.
+    iApply (type_memcpy_iris with "[] [] * [$HEAP $LFT $Htl $HE $HL HT]"); try done.
+    (* TODO: This is kind of silly, why can't I iApply the assumptions directly? *)
+    { iPoseProof Hwrt as "Hwrt". done. }
+    { iPoseProof Hread as "Hread". done. }
     { by rewrite tctx_interp_cons tctx_interp_singleton. }
     rewrite tctx_interp_cons tctx_interp_singleton. auto.
   Qed.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 83c62f5921c8cef04da7f34e443a3d03bd108bc7..789aaa3ee4fee0ddd5124afee2746c195d113625 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -80,7 +80,7 @@ Section typing.
   Lemma read_shr E L κ ty :
     Copy ty → lctx_lft_alive E L κ → typed_read E L (&shr{κ}ty) ty (&shr{κ}ty).
   Proof.
-    iIntros (Hcopy Halive v tid F qE qL ?) "#LFT Htl HE HL Hown".
+    iIntros (Hcopy Halive) "!#". iIntros (v tid F qE qL ?) "#LFT Htl HE HL Hown".
     iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first set_solver.
     iDestruct "Hown" as (l) "[EQ #Hshr]". iDestruct "EQ" as %[=->].
      assert (↑shrN ⊆ (↑lrustN : coPset)) by solve_ndisj. (* set_solver needs some help. *)
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 0e16e21865f518338da2deda1a59ab9ad6af9751..e523544d6f9da6c439304d3a7074da52e44e2485 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -16,7 +16,7 @@ Section case.
       typed_body E L C ((p ◁ own n (sum tyl)) :: T) e) tyl el →
     typed_body E L C ((p ◁ own n (sum tyl)) :: T) (case: !p of el).
   Proof.
-    iIntros (Hel tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
+    iIntros (Hel) "!#". iIntros (tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
     rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
     iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hp".
     iDestruct "Hp" as (l) "[EQ [H↦ Hf]]". iDestruct "EQ" as %[=->].
@@ -66,7 +66,7 @@ Section case.
       typed_body E L C ((p ◁ &uniq{κ}sum tyl) :: T) e) tyl el →
     typed_body E L C ((p ◁ &uniq{κ}sum tyl) :: T) (case: !p of el).
   Proof.
-    iIntros (Halive Hel tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
+    iIntros (Halive Hel) "!#". iIntros (tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
     rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
     iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hp".
     iDestruct "Hp" as (l P) "[[EQ HP] Hb]". iDestruct "EQ" as %[=->].
@@ -123,7 +123,7 @@ Section case.
       typed_body E L C ((p ◁ &shr{κ}sum tyl) :: T) e) tyl el →
     typed_body E L C ((p ◁ &shr{κ}sum tyl) :: T) (case: !p of el).
   Proof.
-    iIntros (Halive Hel tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
+    iIntros (Halive Hel) "!#". iIntros (tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
     rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
     iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hp".
     iDestruct "Hp" as (l) "[EQ Hl]". iDestruct "EQ" as %[=->].
@@ -157,12 +157,12 @@ Section case.
     typed_write E L ty1 (sum tyl) ty2 →
     typed_instruction E L [p1 ◁ ty1; p2 ◁ ty] (p1 <-{i} p2) (λ _, [p1 ◁ ty2]%TC).
   Proof.
-    iIntros (Hty Hw ??) "#HEAP #LFT $ HE HL Hp".
+    iIntros (Hty Hw) "!# * #HEAP #LFT $ HE HL Hp".
     rewrite tctx_interp_cons tctx_interp_singleton.
     iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (closed_hasty with "Hp1") as "%".
     iDestruct (closed_hasty with "Hp2") as "%". wp_bind p1.
     iApply (wp_hasty with "Hp1"). iIntros (v1 Hv1) "Hty1".
-    iMod (Hw with "LFT HE HL Hty1") as (l vl) "(H & H↦ & Hw)"=>//=.
+    iMod (Hw with "* [] LFT HE HL Hty1") as (l vl) "(H & H↦ & Hw)"=>//=.
     destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] ->].
     rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl]".
     wp_write. iApply wp_seq. done. iNext. wp_bind p1.
@@ -184,9 +184,9 @@ Section case.
     typed_write E L ty1 (sum tyl) ty2 →
     typed_instruction E L [p ◁ ty1] (p <-{i} ☇) (λ _, [p ◁ ty2]%TC).
   Proof.
-    iIntros (Hty Hw ??) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
+    iIntros (Hty Hw) "!# * #HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hty".
-    iMod (Hw with "LFT HE HL Hty") as (l vl) "(H & H↦ & Hw)". done.
+    iMod (Hw with "* [] LFT HE HL Hty") as (l vl) "(H & H↦ & Hw)". done.
     simpl. destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] ->].
     rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl]".
     wp_write. rewrite tctx_interp_singleton tctx_hasty_val' //.
@@ -201,18 +201,18 @@ Section case.
     typed_instruction E L [p1 ◁ ty1; p2 ◁ ty2]
                (p1 <⋯{i} !{ty.(ty_size)}p2) (λ _, [p1 ◁ ty1'; p2 ◁ ty2']%TC).
   Proof.
-    iIntros (Hty Hw Hr ??) "#HEAP #LFT Htl [HE1 HE2] [HL1 HL2] Hp".
+    iIntros (Hty Hw Hr) "!# * #HEAP #LFT Htl [HE1 HE2] [HL1 HL2] Hp".
     rewrite tctx_interp_cons tctx_interp_singleton.
     iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (closed_hasty with "Hp1") as "%".
     iDestruct (closed_hasty with "Hp2") as "%". wp_bind p1.
     iApply (wp_hasty with "Hp1"). iIntros (v1 Hv1) "Hty1".
-    iMod (Hw with "LFT HE1 HL1 Hty1") as (l1 vl1) "(H & H↦ & Hw)"=>//=.
+    iMod (Hw with "* [] LFT HE1 HL1 Hty1") as (l1 vl1) "(H & H↦ & Hw)"=>//=.
     destruct vl1 as [|? vl1]; iDestruct "H" as %[[= Hlen] ->].
     rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl1]". wp_write.
     iApply wp_seq. done. iNext. wp_bind p1.
     iApply (wp_wand with "[]"); first by iApply (wp_eval_path). iIntros (? ->).
     wp_op. wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2 Hv2) "Hty2".
-    iMod (Hr with "LFT Htl HE2 HL2 Hty2") as (l2 vl2 q) "(% & H↦2 & Hty & Hr)"=>//=. subst.
+    iMod (Hr with "* [] LFT Htl HE2 HL2 Hty2") as (l2 vl2 q) "(% & H↦2 & Hty & Hr)"=>//=. subst.
     assert (ty.(ty_size) ≤ length vl1).
     { revert i Hty. rewrite Hlen. clear. induction tyl=>//= -[|i] /=.
       - intros [= ->]. lia.
@@ -231,4 +231,4 @@ Section case.
       iExists _. iFrame. rewrite /= drop_length. iPureIntro. lia.
     - iExists _. iFrame.
   Qed.
-End case.
\ No newline at end of file
+End case.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index bc8db8522fcaf7d706d839aa9097d3f860d97fe9..32bc08a56ca8cdbe9e06165c475bf270695261f0 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -213,7 +213,7 @@ Section typing.
   Lemma read_uniq E L κ ty :
     Copy ty → lctx_lft_alive E L κ → typed_read E L (&uniq{κ}ty) ty (&uniq{κ}ty).
   Proof.
-    iIntros (Hcopy Halive v tid F qE qL ?) "#LFT Htl HE HL Hown".
+    iIntros (Hcopy Halive) "!#". iIntros (v tid F qE qL ?) "#LFT Htl HE HL Hown".
     iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first set_solver.
     iDestruct "Hown" as (l P) "[[EQ #HP] H↦]". iDestruct "EQ" as %[=->].
     iMod (bor_iff with "LFT [] H↦") as "H↦". set_solver. by eauto.
@@ -230,7 +230,7 @@ Section typing.
   Lemma write_uniq E L κ ty :
     lctx_lft_alive E L κ → typed_write E L (&uniq{κ}ty) ty (&uniq{κ}ty).
   Proof.
-    iIntros (Halive p tid F qE qL ?) "#LFT HE HL Hown".
+    iIntros (Halive) "!#". iIntros (p tid F qE qL ?) "#LFT HE HL Hown".
     iMod (Halive with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
     iDestruct "Hown" as (l P) "[[EQ #HP] H↦]". iDestruct "EQ" as %[=->].
     iMod (bor_iff with "LFT [] H↦") as "H↦". set_solver. by eauto.