diff --git a/base_logic/lib/boxes.v b/base_logic/lib/boxes.v
index bbefe345fcb4c7a6be3ac0c73478fa96d67afaa1..1d9b5fc94de14a081d9d879ae95d9a9cae9c7f29 100644
--- a/base_logic/lib/boxes.v
+++ b/base_logic/lib/boxes.v
@@ -160,7 +160,7 @@ Proof.
     iFrame; eauto.
 Qed.
 
-Lemma box_fill_all f P Q : box N f P ∗ ▷ P ={N}=∗ box N (const true <$> f) P.
+Lemma box_fill_all f P : box N f P ∗ ▷ P ={N}=∗ box N (const true <$> f) P.
 Proof.
   iIntros "[H HP]"; iDestruct "H" as (Φ) "[#HeqP Hf]".
   iExists Φ; iSplitR; first by rewrite big_sepM_fmap.
@@ -175,7 +175,7 @@ Proof.
   iApply "Hclose". iNext; iExists true. by iFrame.
 Qed.
 
-Lemma box_empty_all f P Q :
+Lemma box_empty_all f P :
   map_Forall (λ _, (true =)) f →
   box N f P ={N}=∗ ▷ P ∗ box N (const false <$> f) P.
 Proof.