Commit 8d7a6268 authored by Dan Frumin's avatar Dan Frumin
Browse files

Simplify a proof

parent 3736872f
......@@ -511,13 +511,7 @@ Section flock.
(Excl' )).
by apply option_local_update, exclusive_local_update. }
(* Get the tokens out of cinvs *)
iDestruct "Hfa" as "(T2 & #Hiinv & Hρ)".
iMod (cinv_open with "Hiinv Hρ") as "(HC & Hρ & Hcl2)". solve_ndisj.
iDestruct "HC" as "[[HR >T1] | >T2']"; last first.
{ iDestruct (own_valid_2 with "T2' T2") as %?. done. }
iMod ("Hcl2" with "[HR T1]") as "_".
{ iNext. iLeft. iFrame. }
iMod ("Hcl" with "[-HΦ Hlocked Hactives Hunflkd Hρ]") as "_".
{ iNext. iExists Unlocked,,(<[i:=ρ]>fp).
Markdown is supported
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