Commit 4ba397e9 authored by Hai Dang's avatar Hai Dang
Browse files

Minor cleanup

parent 6b56559f
......@@ -1748,10 +1748,10 @@ Proof.
rewrite bi.and_elim_r.
set Vpp := mkDView V V2' V2' bLeVV2'.
(* TODO: Local version of [graph_snap_mono] *)
iAssert (@{V2'} StackLocal N γg s G2 M)%I with "[Gs]" as "SL'".
{ iSplit.
- iDestruct "GS2" as "[$ _]". iApply (view_at_mono with "PSV0").
- (* TODO variant of graph_snap_mono *)
iDestruct "GS2" as "[$ _]". iApply (view_at_mono with "PSV0").
+ clear -LeV' LeV1. solve_lat.
+ by apply SeenLogview_map_mono.
- iExists γ, γh. iFrame "MTs SII". iExists T2. iFrame "LT2". iSplitL "".
......
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