diff --git a/base_logic/lib/boxes.v b/base_logic/lib/boxes.v
index 5cbff7ecded0e7c8f6e5ffab278afaa9e46d5653..7cd28246a9fec21a9a50130ccd98b6350061c93c 100644
--- a/base_logic/lib/boxes.v
+++ b/base_logic/lib/boxes.v
@@ -185,9 +185,7 @@ Proof.
   iMod (box_empty with "[$Hslice $Hbox]") as "[$ Hbox]"; try done.
   iMod (box_delete_empty with "[$Hslice $Hbox]") as (P') "[Heq Hbox]".
     done. by apply lookup_insert.
-  iExists P'. rewrite delete_insert. iFrame.
-  iMod (box_fill with "[$Hslice $HQ $Hbox]"). done.
-   by rewrite insert_insert.
+  iExists P'. iFrame. rewrite -insert_delete delete_insert ?lookup_delete //.
 Qed.
 
 Lemma box_fill_all E f P :