Skip to content
Snippets Groups Projects
Commit ff96075a authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Next time I will think about committing something that works...

parent dc432a1f
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 3 deletions
base_logic/lib/boxes.v
+ 1
− 3
View file @ ff96075a
...@@ -185,9 +185,7 @@ Proof. ...@@ -185,9 +185,7 @@ Proof.
iMod (box_empty with "[$Hslice $Hbox]") as "[$ Hbox]"; try done. iMod (box_empty with "[$Hslice $Hbox]") as "[$ Hbox]"; try done.
iMod (box_delete_empty with "[$Hslice $Hbox]") as (P') "[Heq Hbox]". iMod (box_delete_empty with "[$Hslice $Hbox]") as (P') "[Heq Hbox]".
done. by apply lookup_insert. done. by apply lookup_insert.
iExists P'. rewrite delete_insert. iFrame. iExists P'. iFrame. rewrite -insert_delete delete_insert ?lookup_delete //.
iMod (box_fill with "[$Hslice $HQ $Hbox]"). done.
by rewrite insert_insert.
Qed. Qed.
Lemma box_fill_all E f P : Lemma box_fill_all E f P :
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment