diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index 51dbdc4d4a6b0e863427dbaf7087f934f23d65e2..2427e9bad6813296c99ad9f7e42f8c7a97a53408 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -161,7 +161,7 @@ Proof.
   iDestruct (box_own_auth_agree γ b true with "[#]")
     as "%"; subst; first by iFrame "Hγ".
   iFrame "HQ".
-  iPvs (box_own_auth_update _ γ true true false with "[Hγ Hγ']")
+  iPvs (box_own_auth_update _ γ with "[Hγ Hγ']")
     as "[Hγ Hγ']"; first by iFrame "Hγ".
   iPvsIntro; iNext; iSplitL "Hγ"; first (iExists false; by repeat iSplit).
   iExists Φ; iSplit.
@@ -181,7 +181,7 @@ Proof.
   iApply (big_sepM_impl _ _ f); iFrame "Hf".
   iAlways; iIntros {γ b' ?} "[(Hγ' & #$ & #$) HΦ]".
   iInv N as {b} "[Hγ _]"; iTimeless "Hγ".
-  iPvs (box_own_auth_update _ γ b b' true with "[Hγ Hγ']")
+  iPvs (box_own_auth_update _ γ with "[Hγ Hγ']")
     as "[Hγ $]"; first by iFrame "Hγ".
   iPvsIntro; iNext; iExists true. by iFrame "HΦ Hγ".
 Qed.