Commit c9760e26 authored by Robbert Krebbers's avatar Robbert Krebbers

Oops, fix 8d1b743e, forgot something.

parent 8d1b743e
......@@ -191,7 +191,7 @@ Lemma box_empty_all f P Q :
Proof.
iIntros {?} "H"; iDestruct "H" as {Φ} "[#HeqP Hf]".
iAssert ([ map] γ↦b f, Φ γ box_own_auth γ ( Excl' false)
box_own_prop γ (Φ γ) inv N (box_inv γ (Φ γ)))%I with "=>[Hf]" as "[HΦ ?]".
box_own_prop γ (Φ γ) inv N (box_slice_inv γ (Φ γ)))%I with "=>[Hf]" as "[HΦ ?]".
{ iApply (pvs_big_sepM _ _ f); iApply (big_sepM_impl _ _ f); iFrame "Hf".
iAlways; iIntros {γ b ?} "(Hγ' & #$ & #$)".
assert (true = b) as <- by eauto.
......
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