diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index acab5721de896ef4a98dc5e6133df3c45fd83359..0404645e4f9d228bb1dbecca32143d91bcb17292 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -167,7 +167,7 @@ Proof.
     iMod ("Hclose'" with "[-Hbor Hclose]") as "_".
     { iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
       iLeft. iFrame "%". iExists _, _. iFrame. }
-    iExists κ''. iFrame "#". iIntros "!>* HvsQ HQ". clear -HE.
+    iExists κ''. iFrame "#". 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 //
@@ -235,7 +235,7 @@ Proof.
       as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
     iMod (slice_delete_full _ _ true with "Hs Hbox") as (Pb') "(HP' & EQ & Hbox)".
       solve_ndisj. by rewrite lookup_fmap EQB. iDestruct ("HPP'" with "HP'") as "$".
-    iApply fupd_mask_intro; [solve_ndisj|]. iIntros "Hclose * HvsQ HQ".
+    iApply fupd_mask_intro; [solve_ndisj|]. iIntros "Hclose %Q HvsQ HQ".
     iMod "Hclose" as "_". iDestruct (add_vs with "EQ Hvs [HvsQ]") as "Hvs".
     { iNext. iIntros "HQ H†". iApply "HPP'". iApply ("HvsQ" with "HQ H†"). }
     iMod (slice_insert_full _ _ true with "HQ Hbox") as (j) "(% & #Hs' & Hbox)".