diff --git a/base_logic/lib/boxes.v b/base_logic/lib/boxes.v
index 5ecb2d037fc3518a1c7c2048341b3730957a38c8..3ae9b0c7ba297e8176f4a2d0f209ad9a18fd6366 100644
--- a/base_logic/lib/boxes.v
+++ b/base_logic/lib/boxes.v
@@ -85,7 +85,7 @@ Proof.
   - by rewrite big_sepM_empty.
 Qed.
 
-Lemma box_insert E f P Q :
+Lemma box_insert_empty E f P Q :
   ▷ box N f P ={E}=∗ ∃ γ, ⌜f !! γ = None⌝ ∗
     slice N γ Q ∗ ▷ box N (<[γ:=false]> f) (Q ∗ P).
 Proof.
@@ -143,6 +143,18 @@ Proof.
     iFrame; eauto.
 Qed.
 
+Lemma box_insert_full E f P Q :
+  ↑N ⊆ E →
+  ▷ Q ∗ ▷ box N f P ={E}=∗ ∃ γ, ⌜f !! γ = None⌝ ∗
+    slice N γ Q ∗ ▷ box N (<[γ:=true]> f) (Q ∗ P).
+Proof.
+  iIntros (?) "[HQ Hbox]".
+  iMod (box_insert_empty with "Hbox") as (γ) "(% & #Hslice & Hbox)".
+  iExists γ. iFrame "%#".
+  iMod (box_fill with "[$Hslice $HQ $Hbox]"). done.
+  by apply lookup_insert. by rewrite insert_insert.
+Qed.
+
 Lemma box_empty E f P Q γ :
   ↑N ⊆ E →
   f !! γ = Some true →