diff --git a/opam.pins b/opam.pins
index 221e0a3f085dfecaf02f97c9e4afadceb9f74c7e..9db15430a363054e5037c0a9811c84766b3a8405 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq f1b30a2eb12d38bffd8a0aa541c90e3675af2a29
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq ea64fd148b56e1c38c08c2954e76bfa2e75b4db9
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index eecf25ec37e0132a08d43ad84717e448b807971a..a69d2e12221f3638875649ae77854d30105393a9 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -13,7 +13,7 @@ Section bool.
          | [ #(LitInt (0|1))] => True
          | _ => False
          end%I |}.
-  Next Obligation. intros ? [|[[| |[|[]|]]|] []]; try iIntros "[]"; auto. Qed.
+  Next Obligation. intros ? [|[[| |[|[]|]]|] []]; auto with I. Qed.
   Next Obligation. intros ? [|[[| |[|[]|]]|] []]; apply _. Qed.
 
   Global Instance bool_send : Send bool.
@@ -46,8 +46,7 @@ Section typing.
     iIntros (Hp He1 He2) "!#". iIntros (tid qE) "#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 ([[| |[|[]|]]|]) "_ H1"; try iDestruct "H1" as "[]";
-      (iApply wp_case; [done..|iNext]).
+    iIntros ([[| |[|[]|]]|]) "_ H1"; try done; (iApply wp_case; [done..|iNext]).
     - iApply (He2 with "LFT Htl HE HL HC HT").
     - iApply (He1 with "LFT Htl HE HL HC HT").
   Qed.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 2edeb1541076824a6552adcc751ee25d53b248e2..23f73999715715ab8ca11594e7c8bf4472199f6d 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -17,8 +17,8 @@ Section borrow.
   Proof.
     iIntros (tid ??) "#LFT $ $ H".
     rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
-    iDestruct "H" as ([[]|]) "[% Hown]"; try iDestruct "Hown" as "[]".
-    iDestruct "Hown" as "[Hmt ?]". iMod (bor_create with "LFT Hmt") as "[Hbor Hext]". done.
+    iDestruct "H" as ([[]|]) "[% Hown]"; try done. iDestruct "Hown" as "[Hmt ?]".
+    iMod (bor_create with "LFT Hmt") as "[Hbor Hext]". done.
     iModIntro. iSplitL "Hbor".
     - iExists _. auto.
     - iExists _. iSplit. done. by iFrame.
@@ -50,8 +50,7 @@ Section borrow.
     iIntros (Hκ) "!#". iIntros (tid qE) "#LFT $ HE HL Hp".
     rewrite tctx_interp_singleton.
     iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
-    wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown";
-      (try iDestruct "Hown" as "[]").
+    wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
     iMod (bor_acc_cons with "LFT Hown Htok") as "[H↦ Hclose']". done.
     iDestruct "H↦" as ([|[[|l'|]|][]]) "[>H↦ Hown]"; try iDestruct "Hown" as ">[]".
       iDestruct "Hown" as "[Hown H†]". rewrite heap_mapsto_vec_singleton -wp_fupd. wp_read.
@@ -83,8 +82,8 @@ Section borrow.
     iIntros (Hκ) "!#". iIntros (tid qE) "#LFT $ HE HL Hp".
     rewrite tctx_interp_singleton.
     iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
-    wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown";
-      (try iDestruct "Hown" as "[]"). iDestruct "Hown" as (l') "#[H↦b #Hown]".
+    wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
+    iDestruct "Hown" as (l') "#[H↦b #Hown]".
     iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
     iApply (wp_fupd_step _ (_∖_) with "[Hown Htok2]"); try done.
     - iApply ("Hown" with "[%] Htok2"). set_solver+.
@@ -113,8 +112,7 @@ Section borrow.
     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.
-    wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown";
-      try iDestruct "Hown" as "[]".
+    wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
     iMod (bor_exists with "LFT Hown") as (vl) "Hbor". done.
     iMod (bor_sep with "LFT Hbor") as "[H↦ Hbor]". done.
     destruct vl as [|[[]|][]];
@@ -149,8 +147,8 @@ Section borrow.
     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.
-    wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hshr";
-      try iDestruct "Hshr" as "[]". iDestruct "Hshr" as (l') "[H↦ Hown]".
+    wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hshr"; try done.
+    iDestruct "Hshr" as (l') "[H↦ Hown]".
     iMod (frac_bor_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
     iAssert (κ ⊑ κ' ∪ κ)%I as "#Hincl'".
     { iApply (lft_incl_glb with "Hincl []"). iApply lft_incl_refl. }
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 4661019139e9b1dae7ec0fa40e6ba5d6740276de..e179a61b692bf8d0157933bba11154101b209260 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -12,7 +12,7 @@ Section int.
          | [ #(LitInt z)] => True
          | _ => False
          end%I |}.
-  Next Obligation. intros ? [|[[]|] []]; try iIntros "[]". auto. Qed.
+  Next Obligation. intros ? [|[[]|] []]; auto with I. Qed.
   Next Obligation. intros ? [|[[]|] []]; apply _. Qed.
 
   Global Instance int_send : Send int.
@@ -42,10 +42,8 @@ Section typing.
   Proof.
     iAlways. iIntros (tid qE) "_ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
     iIntros "[Hp1 Hp2]".
-    wp_apply (wp_hasty with "Hp1").
-    iIntros ([[]|]) "_ H1"; try iDestruct "H1" as "[]".
-    wp_apply (wp_hasty with "Hp2").
-    iIntros ([[]|]) "_ H2"; try iDestruct "H2" as "[]".
+    wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
+    wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
     wp_op. by rewrite tctx_interp_singleton tctx_hasty_val' //.
   Qed.
 
@@ -63,10 +61,8 @@ Section typing.
   Proof.
     iAlways. iIntros (tid qE) "_ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
     iIntros "[Hp1 Hp2]".
-    wp_apply (wp_hasty with "Hp1").
-    iIntros ([[]|]) "_ H1"; try iDestruct "H1" as "[]".
-    wp_apply (wp_hasty with "Hp2").
-    iIntros ([[]|]) "_ H2"; try iDestruct "H2" as "[]".
+    wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
+    wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
     wp_op. by rewrite tctx_interp_singleton tctx_hasty_val' //.
   Qed.
 
@@ -84,10 +80,8 @@ Section typing.
   Proof.
     iAlways. iIntros (tid qE) "_ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
     iIntros "[Hp1 Hp2]".
-    wp_apply (wp_hasty with "Hp1").
-    iIntros ([[]|]) "_ H1"; try iDestruct "H1" as "[]".
-    wp_apply (wp_hasty with "Hp2").
-    iIntros ([[]|]) "_ H2"; try iDestruct "H2" as "[]".
+    wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
+    wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
     wp_op; intros _; by rewrite tctx_interp_singleton tctx_hasty_val' //.
   Qed.
 
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 32a9fa29f47c77acee4ebb797fd956f7618975cd..e1786c942942bc08b5b6cb192e2edcd6994ec8e5 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -62,7 +62,7 @@ Section own.
          (∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
             □ (∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ] ={F,F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) κ tid l' ∗ q.[κ]))%I
     |}.
-  Next Obligation. by iIntros (q ty tid [|[[]|][]]) "H"; try iDestruct "H" as "[]". Qed.
+  Next Obligation. by iIntros (q ty tid [|[[]|][]]) "H". Qed.
   Next Obligation.
     move=>n ty N κ l tid ?? /=. iIntros "#LFT Hshr Htok".
     iMod (bor_exists with "LFT Hshr") as (vl) "Hb". set_solver.
@@ -102,7 +102,7 @@ Section own.
     type_incl ty1 ty2 -∗ type_incl (own_ptr n ty1) (own_ptr n ty2).
   Proof.
     iIntros "(#Hsz & #Ho & #Hs)". iSplit; first done. iSplit; iAlways.
-    - iIntros (?[|[[| |]|][]]) "H"; try iDestruct "H" as "[]". simpl.
+    - iIntros (?[|[[| |]|][]]) "H"; try done. simpl.
       iDestruct "H" as "[Hmt H†]". iDestruct "Hmt" as (vl') "[Hmt Hown]". iNext.
       iDestruct ("Ho" with "Hown") as "Hown". iDestruct ("Hsz") as %<-.
       iFrame. iExists _. iFrame.
@@ -168,17 +168,15 @@ Section typing.
   Lemma write_own {E L} ty ty' n :
     ty.(ty_size) = ty'.(ty_size) → typed_write E L (own_ptr n ty') ty (own_ptr n ty).
   Proof.
-    iIntros (Hsz) "!#". iIntros ([[]|] tid F qE qL ?) "_ $ $ Hown";
-      try iDestruct "Hown" as "[]". rewrite /= Hsz. iDestruct "Hown" as "[H↦ $]".
-    iDestruct "H↦" as (vl) "[>H↦ Hown]". iDestruct (ty_size_eq with "Hown") as "#>%".
-    iExists _, _. iFrame "H↦". auto.
+    iIntros (Hsz) "!#". iIntros ([[]|] tid F qE 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.
   Qed.
 
   Lemma read_own_copy E L ty n :
     Copy ty → typed_read E L (own_ptr n ty) ty (own_ptr n ty).
   Proof.
-    iIntros (Hsz) "!#". iIntros ([[]|] tid F qE qL ?) "_ $ $ $ Hown";
-      try iDestruct "Hown" as "[]".
+    iIntros (Hsz) "!#". iIntros ([[]|] tid F qE 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.
@@ -187,8 +185,7 @@ Section typing.
   Lemma read_own_move E L ty n :
     typed_read E L (own_ptr n ty) ty (own_ptr n $ uninit ty.(ty_size)).
   Proof.
-    iAlways. iIntros ([[]|] tid F qE qL ?) "_ $ $ $ Hown";
-      try iDestruct "Hown" as "[]".
+    iAlways. iIntros ([[]|] tid F qE qL ?) "_ $ $ $ Hown"; try done.
     iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
     iDestruct (ty_size_eq with "Hown") as "#>%".
     iExists l, vl, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !> !>".
@@ -233,11 +230,10 @@ Section typing.
     typed_instruction E L [p ◁ box ty] (delete [ #n; p])%E (λ _, []).
   Proof.
     iIntros (<-) "!#". iIntros (tid eq) "#LFT $ $ $ Hp". rewrite tctx_interp_singleton.
-    wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown";
-      try iDestruct "Hown" as "[]". iDestruct "Hown" as "[H↦∗: >H†]".
-    iDestruct "H↦∗:" as (vl) "[>H↦ Hown]". rewrite tctx_interp_nil.
-    iDestruct (ty_size_eq with "Hown") as "#>EQ". iDestruct "EQ" as %<-.
-    iApply (wp_delete with "[-]"); try (by auto); [].
+    wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
+    iDestruct "Hown" as "[H↦∗: >H†]". iDestruct "H↦∗:" as (vl) "[>H↦ Hown]".
+    rewrite tctx_interp_nil. iDestruct (ty_size_eq with "Hown") as "#>EQ".
+    iDestruct "EQ" as %<-. iApply (wp_delete with "[-]"); auto; [].
     rewrite freeable_sz_full. by iFrame.
   Qed.
 
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 4e90676d4c49646219fe19f26c06361a30cda1b0..bb7955a0196482307c23045446b18e013fef4262 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -90,7 +90,7 @@ Section product_split.
   Proof.
     iIntros (tid q1 q2) "#LFT $ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
-    iDestruct "H" as ([[]|]) "[#Hp H]"; try iDestruct "H" as "[]".
+    iDestruct "H" as ([[]|]) "[#Hp H]"; try done.
     iDestruct "H" as "[H >H†]". iDestruct "H" as (vl) "[>H↦ H]".
     iDestruct "H" as (vl1 vl2) "(>% & H1 & H2)". subst.
     rewrite heap_mapsto_vec_app -freeable_sz_split.
@@ -108,15 +108,15 @@ Section product_split.
   Proof.
     iIntros (tid q1 q2) "#LFT $ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
-    iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "(Hp1 & H1)";
-      try iDestruct "H1" as "[]". iDestruct "H1" as "(H↦1 & H†1)".
+    iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "(Hp1 & H1)"; try done.
+    iDestruct "H1" as "(H↦1 & H†1)".
     iDestruct "H2" as (v2) "(Hp2 & H2)". simpl. iDestruct "Hp1" as %Hρ1.
     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_mapsto_vec_app. iFrame.
     iDestruct (ty_size_eq with "H1") as "#>EQ". iDestruct "EQ" as %->.
-    iFrame. iExists vl1, vl2. iFrame. auto 10.
+    auto 10 with iFrame.
   Qed.
 
   Lemma tctx_split_own_prod E L n tyl p :
@@ -124,7 +124,7 @@ Section product_split.
   Proof.
     apply tctx_split_ptr_prod.
     - intros. apply tctx_split_own_prod2.
-    - intros ??[|[[]|][]]; try iIntros "[]". eauto.
+    - iIntros (??[|[[]|][]]) "?"; eauto.
   Qed.
 
   Lemma tctx_merge_own_prod E L n tyl :
@@ -135,7 +135,7 @@ Section product_split.
     intros. apply tctx_merge_ptr_prod; try done.
     - apply _.
     - intros. apply tctx_merge_own_prod2.
-    - intros ??[|[[]|][]]; try iIntros "[]". eauto.
+    - iIntros (??[|[[]|][]]) "?"; eauto.
   Qed.
 
   (** Unique borrows *)
@@ -145,7 +145,7 @@ Section product_split.
   Proof.
     iIntros (tid q1 q2) "#LFT $ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
-    iDestruct "H" as ([[]|]) "[Hp H]"; try iDestruct "H" as "[]". iDestruct "Hp" as %Hp.
+    iDestruct "H" as ([[]|]) "[Hp H]"; try done. iDestruct "Hp" as %Hp.
     rewrite /= split_prod_mt. iMod (bor_sep with "LFT H") as "[H1 H2]".
     set_solver. rewrite /tctx_elt_interp /=.
     iSplitL "H1"; iExists _; (iSplitR; first by rewrite Hp); auto.
@@ -157,18 +157,15 @@ Section product_split.
   Proof.
     iIntros (tid q1 q2) "#LFT $ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
-    iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 H1]";
-      try iDestruct "H1" as "[]". iDestruct "Hp1" as %Hp1.
-    iDestruct "H2" as (v2) "(Hp2 & H2)". rewrite /= Hp1. iDestruct "Hp2" as %[=<-].
-    iExists #l. iFrame "%". iMod (bor_combine with "LFT H1 H2") as "H". set_solver.
-    by rewrite /= split_prod_mt.
+    iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 H1]"; try done.
+    iDestruct "Hp1" as %Hp1. iDestruct "H2" as (v2) "(Hp2 & H2)". rewrite /= Hp1.
+    iDestruct "Hp2" as %[=<-]. iExists #l. iFrame "%".
+    iMod (bor_combine with "LFT H1 H2") as "H". set_solver. by rewrite /= split_prod_mt.
   Qed.
 
   Lemma uniq_is_ptr κ ty tid (vl : list val) :
     ty_own (&uniq{κ} ty) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]⌝.
-  Proof.
-    iIntros "H". destruct vl as [|[[]|][]]; try iDestruct "H" as "[]". eauto.
-  Qed.
+  Proof. iIntros "H". destruct vl as [|[[]|][]]; eauto. Qed.
 
   Lemma tctx_split_uniq_prod E L κ tyl p :
     tctx_incl E L [p ◁ &uniq{κ} product tyl]
@@ -208,18 +205,14 @@ Section product_split.
   Proof.
     iIntros (tid q1 q2) "#LFT $ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
-    iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 Hown1]";
-      try iDestruct "Hown1" as "[]". iDestruct "Hp1" as %Hp1.
-    iDestruct "H2" as ([[]|]) "[Hp2 Hown2]"; try iDestruct "Hown2" as "[]".
-      rewrite /= Hp1. iDestruct "Hp2" as %[=<-].
-    iExists #l. by iFrame.
+    iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 Hown1]"; try done.
+    iDestruct "Hp1" as %Hp1. iDestruct "H2" as ([[]|]) "[Hp2 Hown2]"; try done.
+    rewrite /= Hp1. iDestruct "Hp2" as %[=<-]. iExists #l. by iFrame.
   Qed.
 
   Lemma shr_is_ptr κ ty tid (vl : list val) :
     ty_own (&shr{κ} ty) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]⌝.
-  Proof.
-    iIntros "H". destruct vl as [|[[]|][]]; try iDestruct "H" as "[]". eauto.
-  Qed.
+  Proof. iIntros "H". destruct vl as [|[[]|][]]; eauto. Qed.
 
   Lemma tctx_split_shr_prod E L κ tyl p :
     tctx_incl E L [p ◁ &shr{κ} product tyl]
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index a0c649a937e02f023576a0eb834b7229348f764e..8ed4d9371c95fa47f05421849fa575288e8b84d4 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -13,16 +13,14 @@ Section shr_bor.
          | [ #(LitLoc l) ] => ty.(ty_shr) κ tid l
          | _ => False
          end%I |}.
-  Next Obligation.
-    iIntros (κ ty tid [|[[]|][]]) "H"; try iDestruct "H" as "[]". done.
-  Qed.
+  Next Obligation. by iIntros (κ ty tid [|[[]|][]]) "H". Qed.
   Next Obligation. intros κ ty tid [|[[]|][]]; apply _. Qed.
 
   Global Instance shr_mono E L :
     Proper (flip (lctx_lft_incl E L) ==> subtype E L ==> subtype E L) shr_bor.
   Proof.
     intros κ1 κ2 Hκ ty1 ty2 Hty. apply subtype_simple_type.
-    iIntros (? [|[[]|][]]) "#LFT #HE #HL H"; try iDestruct "H" as "[]".
+    iIntros (? [|[[]|][]]) "#LFT #HE #HL H"; try done.
     iDestruct (Hκ with "HE HL") as "#Hκ". iApply (ty2.(ty_shr_mono) with "LFT Hκ").
     iDestruct (Hty with "[] [] []") as "(_ & _ & #Hs1)"; [done..|clear Hty].
     by iApply "Hs1".
@@ -44,9 +42,7 @@ Section shr_bor.
 
   Global Instance shr_send κ ty :
     Sync ty → Send (shr_bor κ ty).
-  Proof.
-    iIntros (Hsync tid1 tid2 [|[[]|][]]) "H"; try iDestruct "H" as "[]". by iApply Hsync.
-  Qed.
+  Proof. by iIntros (Hsync tid1 tid2 [|[[]|][]]) "H"; try iApply Hsync. Qed.
 End shr_bor.
 
 Notation "&shr{ κ } ty" := (shr_bor κ ty)
@@ -72,8 +68,7 @@ Section typing.
     iDestruct (llctx_interp_persist with "HL") as "#HL'". iFrame "HE HL".
     iDestruct (Hκκ' with "HE' HL'") as "Hκκ'".
     rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
-    iDestruct "H" as ([[]|]) "[% #Hshr]"; try iDestruct "Hshr" as "[]".
-    iModIntro. iSplit.
+    iDestruct "H" as ([[]|]) "[% #Hshr]"; try done. iModIntro. iSplit.
     - iExists _. iSplit. done. by iApply (ty_shr_mono with "LFT Hκκ' Hshr").
     - iExists _. auto.
   Qed.
@@ -81,8 +76,8 @@ 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) "!#". iIntros ([[]|] tid F qE qL ?) "#LFT Htl HE HL #Hshr";
-      try iDestruct "Hshr" as "[]".
+    iIntros (Hcopy Halive) "!#".
+    iIntros ([[]|] tid F qE qL ?) "#LFT Htl HE HL #Hshr"; try done.
     iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first set_solver.
     assert (↑shrN ⊆ (↑lrustN : coPset)) by solve_ndisj. (* set_solver needs some help. *)
     iMod (copy_shr_acc with "LFT Hshr Htl Hκ") as (q') "(Htl & H↦ & Hcl)".
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 0c28c7f3949aa606f0cc0963762db2d298a45425..2b7b157df5c2484ad63e18ef7d74ca06af442e98 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -19,17 +19,12 @@ Section sum.
     iMod (bor_acc with "LFT Hown Htok") as "[>H _]"; first done.
     iDestruct "H" as (?) "[_ []]".
   Qed.
-  Next Obligation.
-    iIntros (κ κ' tid l) "#LFT #Hord []".
-  Qed.
+  Next Obligation. iIntros (κ κ' tid l) "#LFT #Hord []". Qed.
 
   Global Instance emp_empty : Empty type := emp.
 
   Global Instance emp_copy : Copy ∅.
-  Proof.
-    split; first by apply _.
-    iIntros (????????) "? []".
-  Qed.
+  Proof. split; first by apply _. iIntros (????????) "? []". Qed.
 
   Global Instance emp_send : Send ∅.
   Proof. iIntros (???) "[]". Qed.
@@ -168,9 +163,8 @@ Section sum.
     - iIntros (??) "[]".
     - iIntros (κ tid l) "[]".
     - iIntros (??) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
-      rewrite nth_empty. by iDestruct "Hown" as "[]".
-    - iIntros (???) "H". iDestruct "H" as (i) "(_ & Hshr)".
-      rewrite nth_empty. by iDestruct "Hshr" as "[]".
+      by rewrite nth_empty.
+    - iIntros (???) "H". iDestruct "H" as (i) "(_ & Hshr)". by rewrite nth_empty.
   Qed.
 
   Global Instance sum_copy tyl : LstCopy tyl → Copy (sum tyl).
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index dc0d11b991dcdd6f9289aae7033da0e3a439a3d3..c1eb039300efc46abfd6df82cace6974198c4b85 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -56,8 +56,7 @@ Section type_context.
     destruct (eval_path p1); try (intros ?; by iApply wp_value); [].
     destruct v0; try discriminate; [].
     destruct l; try discriminate; [].
-    intros [=<-]. iStartProof. wp_bind p1.
-    iApply (wp_wand with "[]").
+    intros [=<-]. wp_bind p1. iApply (wp_wand with "[]").
     { iApply IHp1. done. }
     iIntros (v) "%". subst v. wp_op. done.
   Qed.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 7fa40e162e4dba93c6f48f024a82a4241ef52730..1cc5221c5ccbaa5ff2c00b15ee36b786b02f2df5 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -17,9 +17,8 @@ Section case.
   Proof.
     iIntros (Hel) "!#". iIntros (tid qE) "#LFT Hna HE HL HC HT". wp_bind p.
     rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
-    iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp";
-      try iDestruct "Hp" as "[]". iDestruct "Hp" as "[H↦ Hf]".
-    iDestruct "H↦" as (vl) "[H↦ Hown]".
+    iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try done.
+    iDestruct "Hp" as "[H↦ Hf]". iDestruct "H↦" as (vl) "[H↦ Hown]".
     iDestruct "Hown" as (i vl' vl'') "(>% & >EQlen & Hown)". subst.
     simpl ty_size. iDestruct "EQlen" as %[=EQlen]. rewrite -EQlen. simpl length.
     rewrite -Nat.add_1_l app_length -!freeable_sz_split
@@ -116,12 +115,12 @@ Section case.
   Proof.
     iIntros (Halive Hel) "!#". iIntros (tid qE) "#LFT Hna HE HL HC HT". wp_bind p.
     rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
-    iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try iDestruct "Hp" as "[]".
+    iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try done.
     iDestruct "Hp" as (i) "[#Hb Hshr]".
     iMod (Halive with "HE HL") as (q) "[Htok Hclose]". done.
     iMod (frac_bor_acc with "LFT Hb Htok") as (q') "[[H↦i H↦vl''] Hclose']". done.
     rewrite nth_lookup.
-    destruct (tyl !! i) as [ty|] eqn:EQty; last iDestruct "Hshr" as "[]".
+    destruct (tyl !! i) as [ty|] eqn:EQty; last done.
     edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
     wp_read. iApply wp_case; [lia|by rewrite Nat2Z.id|]. iNext.
     iMod ("Hclose'" with "[$H↦i $H↦vl'']") as "Htok".
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 52e708ffe0a5fe9732b0f78efa8be5e1fbf01ec6..88055127b5897ca6a70289dd531a765ec2382ab9 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -21,9 +21,7 @@ Section uniq_bor.
             □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ∪κ']
                 ={F, F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) (κ∪κ') tid l' ∗ q.[κ∪κ'])%I
     |}.
-  Next Obligation.
-    iIntros (q ty tid [|[[]|][]]) "H"; try iDestruct "H" as "[]". done.
-  Qed.
+  Next Obligation. by iIntros (q ty tid [|[[]|][]]) "H". Qed.
   Next Obligation.
     move=> κ ty N κ' l tid ??/=. iIntros "#LFT Hshr Htok".
     iMod (bor_exists with "LFT Hshr") as ([|[[|l'|]|][]]) "Hb"; first set_solver;
@@ -63,7 +61,7 @@ Section uniq_bor.
     intros κ1 κ2 Hκ ty1 ty2 Hty%eqtype_unfold. iIntros. iSplit; first done.
     iDestruct (Hty with "[] [] []") as "(_ & #Ho & #Hs)"; [done..|clear Hty].
     iDestruct (Hκ with "[] []") as "#Hκ"; [done..|]. iSplit; iAlways.
-    - iIntros (? [|[[]|][]]) "H"; try iDestruct "H" as "[]".
+    - iIntros (? [|[[]|][]]) "H"; try done.
       iApply (bor_shorten with "Hκ"). iApply bor_iff; last done.
       iSplit; iIntros "!>!# H"; iDestruct "H" as (vl) "[??]";
       iExists vl; iFrame; by iApply "Ho".
@@ -95,7 +93,7 @@ Section uniq_bor.
   Global Instance uniq_send κ ty :
     Send ty → Send (uniq_bor κ ty).
   Proof.
-    iIntros (Hsend tid1 tid2 [|[[]|][]]) "H"; try iDestruct "H" as "[]".
+    iIntros (Hsend tid1 tid2 [|[[]|][]]) "H"; try done.
     iApply bor_iff; last done. iNext. iAlways. iApply uPred.equiv_iff.
     do 3 f_equiv. iSplit; iIntros "."; by iApply Hsend.
   Qed.
@@ -130,7 +128,7 @@ Section typing.
     iIntros (Hκ ???) "#LFT HE HL Huniq".
     iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; [try done..|].
     rewrite !tctx_interp_singleton /=.
-    iDestruct "Huniq" as ([[]|]) "[% Huniq]"; try iDestruct "Huniq" as "[]".
+    iDestruct "Huniq" as ([[]|]) "[% Huniq]"; try done.
     iMod (ty.(ty_share) with "LFT Huniq Htok") as "[Hown Htok]"; [solve_ndisj|].
     iMod ("Hclose" with "Htok") as "[$ $]". iExists _. by iFrame "%∗".
   Qed.
@@ -144,7 +142,7 @@ Section typing.
     iDestruct (llctx_interp_persist with "HL") as "#HL'". iFrame "HE HL".
     iDestruct (Hκκ' with "HE' HL'") as "Hκκ'".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
-    iDestruct "H" as ([[]|]) "[% Hb]"; try iDestruct "Hb" as "[]".
+    iDestruct "H" as ([[]|]) "[% Hb]"; try done.
     iMod (rebor with "LFT Hκκ' Hb") as "[Hb Hext]". done. iModIntro.
     iSplitL "Hb"; iExists _; auto.
   Qed.
@@ -191,8 +189,8 @@ 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) "!#". iIntros ([[]|] tid F qE qL ?) "#LFT Htl HE HL Hown";
-      try iDestruct "Hown" as "[]".
+    iIntros (Hcopy Halive) "!#".
+    iIntros ([[]|] tid F qE qL ?) "#LFT Htl HE HL Hown"; try done.
     iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first set_solver.
     iMod (bor_acc with "LFT Hown Hκ") as "[H↦ Hclose']"; first set_solver.
     iDestruct "H↦" as (vl) "[>H↦ #Hown]".
@@ -205,8 +203,8 @@ 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) "!#". iIntros ([[]|] tid F qE qL ?) "#LFT HE HL Hown";
-      try iDestruct "Hown" as "[]".
+    iIntros (Halive) "!#".
+    iIntros ([[]|] tid F qE qL ?) "#LFT HE HL Hown"; try done.
     iMod (Halive with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
     iMod (bor_acc with "LFT Hown Htok") as "[H↦ Hclose']". set_solver.
     iDestruct "H↦" as (vl) "[>H↦ Hown]". rewrite ty.(ty_size_eq).
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index de4f81a8e5890e218ca93729a4971e8690898acb..f3009fae66883bb4d4f1edf40e8e3641322e7246 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -155,9 +155,8 @@ Section typing.
     rewrite 3!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iIntros "(Hr & Hc & #Hc' & Hx)".
     rewrite {1}/elctx_interp big_opL_singleton /=.
-    destruct c' as [[|c'|]|]; try iDestruct "Hc'" as "[]".
-    destruct x as [[|x|]|]; try iDestruct "Hx" as "[]".
-    destruct r as [[|r|]|]; try iDestruct "Hr" as "[]".
+    destruct c' as [[|c'|]|]; try done. destruct x as [[|x|]|]; try done.
+    destruct r as [[|r|]|]; try done.
     iMod (na_bor_acc with "LFT Hc' HE Htl") as "(Hc'↦ & Htl & Hclose)"; [solve_ndisj..|].
     iDestruct "Hc'↦" as (vc') "[>Hc'↦ Hc'own]".
     iDestruct (ty_size_eq with "Hc'own") as "#>%".
diff --git a/theories/typing/unsafe/refcell/ref.v b/theories/typing/unsafe/refcell/ref.v
index d3ccd14b75cc34338d83f795471c2295ac7573a6..93e7cf567fcdc21c8b32e5301754a2eb106d6461 100644
--- a/theories/typing/unsafe/refcell/ref.v
+++ b/theories/typing/unsafe/refcell/ref.v
@@ -27,9 +27,7 @@ Section ref.
              ▷ ty.(ty_shr) (α ∪ ν) tid lv ∗
              ▷ (α ⊑ β) ∗ ▷ &na{β, tid, refcell_invN}(refcell_inv tid lrc γ β ty') ∗
              &na{κ, tid, refcell_refN}(own γ (◯ reading_st q ν)) |}%I.
-  Next Obligation.
-    iIntros (???[|[[]|][|[[]|][]]]); try iIntros "[]"; auto.
-  Qed.
+  Next Obligation. iIntros (???[|[[]|][|[[]|][]]]) "?"; auto. Qed.
   Next Obligation.
     iIntros (α ty E κ l tid q ?) "#LFT Hb Htok".
     iMod (bor_exists with "LFT Hb") as (vl) "Hb". done.
@@ -79,7 +77,7 @@ Section ref.
     iDestruct (Hα with "HE HL") as "Hα1α2".
     iSplit; [|iSplit; iAlways].
     - done.
-    - iIntros (tid [|[[]|][|[[]|][]]]); try iIntros "[]". iIntros "H".
+    - iIntros (tid [|[[]|][|[[]|][]]]) "H"; try done.
       iDestruct "H" as (ν q γ β ty') "(#Hshr & #H⊑ & #Hinv & Htok & Hown)".
       iExists ν, q, γ, β, ty'. iFrame "∗#". iSplit.
       + iApply ty_shr_mono; last by iApply "Hs". done.
diff --git a/theories/typing/unsafe/refcell/ref_code.v b/theories/typing/unsafe/refcell/ref_code.v
index a495552d3d931fd9dde67f74d23c687f81dec5a0..fc845d10a8f6958f0653d84690c9c46aa1b1edd8 100644
--- a/theories/typing/unsafe/refcell/ref_code.v
+++ b/theories/typing/unsafe/refcell/ref_code.v
@@ -63,8 +63,7 @@ Section ref_functions.
     eapply type_deref; [solve_typing..|by apply read_own_move|done|]=>x'.
     iIntros "!# * #LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
-    iDestruct "HT" as "[Hx Hx']".
-    destruct x' as [[|lx'|]|]; try iDestruct "Hx'" as "[]".
+    iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
     iDestruct "Hx'" as (ν q γ δ ty' lv lrc) "#(Hαν & Hfrac & Hshr & Hβδ & Hinv & H◯inv)".
     wp_op. rewrite {1}/elctx_interp big_sepL_cons big_sepL_singleton.
     iDestruct "HE" as "[[Hα1 Hα2] Hβ]".
@@ -128,8 +127,7 @@ Section ref_functions.
     eapply type_deref; [solve_typing..|by apply read_own_move|done|]=>x'.
     iIntros "!# * #LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
-    iDestruct "HT" as "[Hx Hx']".
-    destruct x' as [[|lx'|]|]; try iDestruct "Hx'" as "[]".
+    iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
     iDestruct "Hx'" as (ν q γ δ ty' lv lrc) "#(Hαν & Hfrac & Hshr & Hx')".
     rewrite {1}/elctx_interp 2!big_sepL_cons big_sepL_singleton.
     iDestruct "HE" as "(Hα & Hβ & #Hαβ)".
@@ -165,7 +163,7 @@ Section ref_functions.
     eapply type_fn; [solve_typing..|]=>- /= α ret arg. inv_vec arg=>x. simpl_subst.
     iIntros "!# * #LFT Hna Hα HL Hk Hx".
     rewrite {1}/elctx_interp big_sepL_singleton tctx_interp_singleton tctx_hasty_val.
-    destruct x as [[|lx|]|]; try iDestruct "Hx" as "[]". iDestruct "Hx" as "[Hx Hx†]".
+    destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
     iDestruct "Hx" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Hx"; try iDestruct "Hx" as "[_ >[]]".
     rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
     iDestruct "Hx" as "[[Hx↦1 Hx↦2] Hx]". wp_op. wp_read. wp_let.
diff --git a/theories/typing/unsafe/refcell/refcell_code.v b/theories/typing/unsafe/refcell/refcell_code.v
index e83ebfc6a26dc3c7dd314cf4b190cd390e29a829..53185ea835ba4f9972b0b89b391c6548f9e9bf88 100644
--- a/theories/typing/unsafe/refcell/refcell_code.v
+++ b/theories/typing/unsafe/refcell/refcell_code.v
@@ -28,10 +28,9 @@ Section refcell_functions.
     iIntros (r) "!# * #LFT Hna HE HL Hk HT". simpl_subst.
     rewrite (Nat2Z.id (S ty.(ty_size))) tctx_interp_cons
             tctx_interp_singleton !tctx_hasty_val.
-    iDestruct "HT" as "[Hr Hx]".
-    destruct x as [[|lx|]|]; try iDestruct "Hx" as "[]". iDestruct "Hx" as "[Hx Hx†]".
-    iDestruct "Hx" as (vl) "[Hx↦ Hx]".
-    destruct r as [[|lr|]|]; try iDestruct "Hr" as "[]". iDestruct "Hr" as "[Hr Hr†]".
+    iDestruct "HT" as "[Hr Hx]". destruct x as [[|lx|]|]; try done.
+    iDestruct "Hx" as "[Hx Hx†]". iDestruct "Hx" as (vl) "[Hx↦ Hx]".
+    destruct r as [[|lr|]|]; try done. iDestruct "Hr" as "[Hr Hr†]".
     iDestruct "Hr" as (vl') "Hr". rewrite uninit_own.
     iDestruct "Hr" as "[Hr↦ >SZ]". destruct vl' as [|]; iDestruct "SZ" as %[=].
     rewrite heap_mapsto_vec_cons. iDestruct "Hr↦" as "[Hr↦0 Hr↦1]". wp_op.
@@ -66,10 +65,10 @@ Section refcell_functions.
     iIntros (r) "!# * #LFT Hna HE HL Hk HT". simpl_subst.
     rewrite (Nat2Z.id (ty.(ty_size))) tctx_interp_cons
             tctx_interp_singleton !tctx_hasty_val.
-    iDestruct "HT" as "[Hr Hx]". destruct x as [[|lx|]|]; try iDestruct "Hx" as "[]".
+    iDestruct "HT" as "[Hr Hx]". destruct x as [[|lx|]|]; try done.
     iDestruct "Hx" as "[Hx Hx†]".
     iDestruct "Hx" as ([|[[]|]vl]) "[Hx↦ Hx]"; try iDestruct "Hx" as ">[]".
-    destruct r as [[|lr|]|]; try iDestruct "Hr" as "[]". iDestruct "Hr" as "[Hr Hr†]".
+    destruct r as [[|lr|]|]; try done. iDestruct "Hr" as "[Hr Hr†]".
     iDestruct "Hr" as (vl') "Hr". rewrite uninit_own heap_mapsto_vec_cons.
     iDestruct "Hr" as "[Hr↦ >%]". iDestruct "Hx↦" as "[Hx↦0 Hx↦1]". wp_op.
     iDestruct "Hx" as "[% Hx]". iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
@@ -109,7 +108,7 @@ Section refcell_functions.
         rewrite heap_mapsto_vec_cons.
         iDestruct "H" as "[H1 H2]". iDestruct "H↦" as "[H↦1 H↦2]".
         iSplitL "H1 H↦1"; eauto. iExists _. iFrame. }
-    destruct x as [[|lx|]|]; try iDestruct "Hx" as "[]". iDestruct "Hx" as "[Hx Hx†]".
+    destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
     iDestruct "Hx" as (vl) "[Hx↦ Hx]". rewrite uninit_own. wp_op.
     iApply (type_type _ _ _
             [ #lx ◁ box (uninit 1); #(shift_loc lx' 1) ◁ &uniq{α}ty]%TC
@@ -154,8 +153,7 @@ Section refcell_functions.
     eapply type_deref; [solve_typing..|apply read_own_copy, _|done|].
     iIntros (x') "!# * #LFT Hna HE HL Hk HT". simpl_subst.
     rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
-    iDestruct "HT" as "(Hx & Hx' & Hr)".
-    destruct x' as [[|lx|]|]; try iDestruct "Hx'" as "[]".
+    iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]; try done.
     iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
     rewrite {1}/elctx_interp big_sepL_singleton.
     iMod (lft_incl_acc with "Hαβ HE") as (qβ) "[[Hβtok1 Hβtok2] Hclose]". done.
@@ -261,8 +259,7 @@ Section refcell_functions.
     eapply type_deref; [solve_typing..|apply read_own_copy, _|done|].
     iIntros (x') "!# * #LFT Hna HE HL Hk HT". simpl_subst.
     rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
-    iDestruct "HT" as "(Hx & Hx' & Hr)".
-    destruct x' as [[|lx|]|]; try iDestruct "Hx'" as "[]".
+    iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]; try done.
     iDestruct "Hx'" as (β γ) "#[Hαβ Hinv]".
     rewrite {1}/elctx_interp big_sepL_singleton.
     iMod (lft_incl_acc with "Hαβ HE") as (qβ) "[Hβtok Hclose]". done.
diff --git a/theories/typing/unsafe/refcell/refmut.v b/theories/typing/unsafe/refcell/refmut.v
index db6c45d0aca621235a59cd3dd7135da0bcc22701..3817d1ad94d94ded1606435b6e534baf1b00bc0f 100644
--- a/theories/typing/unsafe/refcell/refmut.v
+++ b/theories/typing/unsafe/refcell/refmut.v
@@ -95,7 +95,7 @@ Section refmut.
     iDestruct (Hα with "HE HL") as "Hα1α2".
     iSplit; [|iSplit; iAlways].
     - done.
-    - iIntros (tid [|[[]|][|[[]|][]]]); try iIntros "[]". iIntros "H".
+    - iIntros (tid [|[[]|][|[[]|][]]]) "H"; try done.
       iDestruct "H" as (ν γ β ty') "(Hb & #H⊑ & #Hinv & Hν & Hown)".
       iExists ν, γ, β, ty'. iFrame "∗#". iSplit.
       + iApply bor_shorten; last iApply bor_iff; last done.
diff --git a/theories/typing/unsafe/refcell/refmut_code.v b/theories/typing/unsafe/refcell/refmut_code.v
index 04e083f85d7140931f78fa845476900b32c1bd45..cfb17aa0fc62803aa344d9db69ec57056f9a97f8 100644
--- a/theories/typing/unsafe/refcell/refmut_code.v
+++ b/theories/typing/unsafe/refcell/refmut_code.v
@@ -30,8 +30,7 @@ Section refmut_functions.
     eapply type_deref; [solve_typing..|by apply read_own_move|done|]=>x'.
     iIntros "!# * #LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
-    iDestruct "HT" as "[Hx Hx']".
-    destruct x' as [[|lx'|]|]; try iDestruct "Hx'" as "[]".
+    iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
     iDestruct "Hx'" as (lv lrc) "#(Hfrac & #Hshr)".
     rewrite {1}/elctx_interp 2!big_sepL_cons big_sepL_singleton.
     iDestruct "HE" as "([Hα1 Hα2] & Hβ & #Hαβ)".
@@ -74,8 +73,7 @@ Section refmut_functions.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']".
     rewrite {1}/elctx_interp 2!big_sepL_cons big_sepL_singleton.
-    iDestruct "HE" as "(Hα & Hβ & #Hαβ)".
-    destruct x' as [[|lx'|]|]; try iDestruct "Hx'" as "[]".
+    iDestruct "HE" as "(Hα & Hβ & #Hαβ)". destruct x' as [[|lx'|]|]; try done.
     iMod (bor_exists with "LFT Hx'") as (vl) "H". done.
     iMod (bor_sep with "LFT H") as "[H↦ H]". done.
     destruct vl as [|[[|lv|]|][|[[|lrc|]|][]]];
@@ -125,7 +123,7 @@ Section refmut_functions.
     eapply type_fn; [solve_typing..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
     iIntros "!# * #LFT Hna Hα HL Hk Hx".
     rewrite {1}/elctx_interp big_sepL_singleton tctx_interp_singleton tctx_hasty_val.
-    destruct x as [[|lx|]|]; try iDestruct "Hx" as "[]". iDestruct "Hx" as "[Hx Hx†]".
+    destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
     iDestruct "Hx" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Hx"; try iDestruct "Hx" as "[_ >[]]".
     rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
     iDestruct "Hx" as "[[Hx↦1 Hx↦2] Hx]". wp_op. wp_read. wp_let.
diff --git a/theories/typing/unsafe/spawn.v b/theories/typing/unsafe/spawn.v
index 56a50af553e1a3ef256b59528dcf4dfd6437a529..656a167d7142ddce391170b5dc2d16833daa45b4 100644
--- a/theories/typing/unsafe/spawn.v
+++ b/theories/typing/unsafe/spawn.v
@@ -22,7 +22,7 @@ Section join_handle.
          | _ => False
          end%I;
        ty_shr κ tid l := True%I |}.
-  Next Obligation. by iIntros (ty tid [|[[]|][]]) "H"; try iDestruct "H" as "[]". Qed.
+  Next Obligation. by iIntros (ty tid [|[[]|][]]) "H". Qed.
   Next Obligation. iIntros "* _ _ _ $". auto. Qed.
   Next Obligation. iIntros (?) "**"; auto. Qed.
 
@@ -30,7 +30,7 @@ Section join_handle.
     type_incl ty1 ty2 -∗ type_incl (join_handle ty1) (join_handle ty2).
   Proof.
     iIntros "#Hincl". iSplit; first done. iSplit; iAlways.
-    - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try by iDestruct "Hvl" as "[]".
+    - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
       iDestruct "Hvl" as (ty) "[Hincl' ?]". iExists ty. iFrame.
       iApply (type_incl_trans with "Hincl'"). done.
     - iIntros "* _". auto.
@@ -73,7 +73,8 @@ Section spawn.
     { (* The core of the proof: showing that spawn is safe. *)
       iAlways. iIntros (tid qE) "#LFT $ $ $".
       rewrite tctx_interp_cons tctx_interp_singleton.
-      iIntros "[Hf' Henv]". iApply (spawn_spec _ (join_inv retty tid) with "[-]"); first solve_to_val; last first; last simpl_subst.
+      iIntros "[Hf' Henv]". iApply (spawn_spec _ (join_inv retty tid) with "[-]");
+                              first solve_to_val; last first; last simpl_subst.
       { iIntros "!> *". rewrite tctx_interp_singleton tctx_hasty_val.
         iIntros "?". iExists retty. iFrame. iApply type_incl_refl. }
       iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let. wp_let.
@@ -119,8 +120,7 @@ Section spawn.
                          (T2 := λ r, [r ◁ box retty]%TC); try solve_typing; [|].
     { iAlways. iIntros (tid qE) "#LFT $ $ $".
       rewrite tctx_interp_singleton tctx_hasty_val. iIntros "Hc'".
-      destruct c' as [[|c'|]|]; try by iDestruct "Hc'" as "[]".
-      iDestruct "Hc'" as (ty') "[#Hsub Hc']".
+      destruct c' as [[|c'|]|]; try done. iDestruct "Hc'" as (ty') "[#Hsub Hc']".
       iApply (join_spec with "Hc'"). iIntros "!> * Hret".
       rewrite tctx_interp_singleton tctx_hasty_val.
       iPoseProof "Hsub" as "Hsz". iDestruct "Hsz" as "[% _]".