Commit 67a102f5 authored by Hai Dang's avatar Hai Dang
Browse files

Remove more TODO

parent d8e78bef
...@@ -141,7 +141,7 @@ Proof. ...@@ -141,7 +141,7 @@ Proof.
iAuIntro. iAuIntro.
iDestruct "I" as (G) "(>I & >GA & Ps)". iDestruct "I" as (G) "(>I & >GA & Ps)".
iApply (aacc_aupd with "AU"); [solve_ndisj|]. iApply (aacc_aupd with "AU"); [solve_ndisj|].
(* TODO: we cannot access eventgraph_consistent for G *) (* We do not have access eventgraph_consistent for G *)
(* connecting our invariant and the AU *) (* connecting our invariant and the AU *)
iIntros (G') "[>I' P]". iIntros (G') "[>I' P]".
iDestruct (ExchangerInv_agree with "I I'") as %->. iDestruct (ExchangerInv_agree with "I I'") as %->.
Supports Markdown
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