diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index e3864ebdf84cbf51ac0766356ca7bb785605303a..bac68ad60daaffc26752a8434468f73431b027e7 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -52,7 +52,7 @@ Section na_bor.
 
   Lemma na_bor_shorten κ κ': κ ⊑ κ' -∗ &na{κ',tid,N}P -∗ &na{κ,tid,N}P.
   Proof.
-    iIntros "Hκκ' H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
+    iIntros "Hκκ' H". iDestruct "H" as (i) "[H ?]". iExists i. iFrame.
     iApply (idx_bor_shorten with "Hκκ' H").
   Qed.
 
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 5b7d94c9dc913621f104355ed2e00c22429e901c..efdb9d10f8f207e93d9a98ca726d39306ad520e9 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -127,7 +127,7 @@ Section refcell.
     iAssert ((q / 2).[κ] ∗ ▷ ∃ γ, refcell_inv tid l γ κ ty)%I with "[> -Hclose]"
       as "[$ HQ]"; last first.
     { iMod ("Hclose" with "[] HQ") as "[Hb $]".
-      - iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(? & _ & _)".
+      - iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(H & _ & _)".
         iExists _. iIntros "{$H}!%". destruct st as [[?[|[]|]]|]; simpl; lia.
       - iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
         iExists κ, γ. iSplitR. by iApply lft_incl_refl. by iApply bor_na. }
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 6b42693d15983748259cfc2ac43edf72cb27233e..67d1092e49d822318192aec87deb5289424992ce 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -122,7 +122,7 @@ Section rwlock.
     iAssert ((q / 2).[κ] ∗ ▷ ∃ γ, rwlock_inv tid l γ κ ty)%I with "[> -Hclose]"
       as "[$ HQ]"; last first.
     { iMod ("Hclose" with "[] HQ") as "[Hb $]".
-      - iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(? & _ & _)".
+      - iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(H & _ & _)".
         iExists _. iIntros "{$H}!%". destruct st as [[|[[]?]|]|]; simpl; lia.
       - iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
         iExists κ, γ. iSplitR. by iApply lft_incl_refl. iApply bor_share; try done.