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

Improve proof.

parent 3401f1b3
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/lifetime/borrow.v
+ 1
− 2
View file @ df4bb25b
......@@ -127,8 +127,7 @@ Proof.
as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
iMod (box_split with "Hslice Hbox") as (γ1 γ2) "(% & % & % & Hs1 & Hs2 & Hbox)".
solve_ndisj. by rewrite lookup_fmap EQB.
iCombine "Hown" "Hbor" as "Hbor". rewrite -own_bor_op.
iMod (own_bor_update with "Hbor") as "Hbor".
iMod (own_bor_update_2 with "Hown Hbor") as "Hbor".
{ etrans; last etrans.
- apply auth_update_dealloc. by apply delete_singleton_local_update, _.
- apply auth_update_alloc,
......
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