Commit 0268fd31 authored by Robbert Krebbers's avatar Robbert Krebbers


parent c3c39389
Pipeline #2664 passed with stage
in 9 minutes and 1 second
......@@ -83,8 +83,8 @@ Section proofs.
iIntros "!==>[HP $]".
iInv tlN as "[[_ >Hdis2]|>Hitok]" "Hclose".
+ iCombine "Hdis" "Hdis2" as "Hdis".
iDestruct (own_valid with "Hdis") as %[_ Hval].
revert Hval. rewrite gset_disj_valid_op. set_solver.
iDestruct (own_valid with "Hdis") as %[_ Hval%gset_disj_valid_op].
+ iFrame. iApply "Hclose". iNext. iLeft. by iFrame.
- iDestruct (tl_own_disjoint tid {[i]} {[i]} with "[-]") as %?; first by iFrame.
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