Commit bbda866b authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

USeless spaces

parent 11736f5e
Pipeline #2608 passed with stage
in 4 minutes and 14 seconds
......@@ -80,7 +80,7 @@ Section proofs.
iIntros (??) "#Htlinv Htoks".
iDestruct "Htlinv" as (i) "[% #Hinv]".
rewrite {1 4}(union_difference_L (nclose N) E) //.
rewrite {1 5}(union_difference_L {[i]} (nclose N)) ?tl_tokens_union; try set_solver.
rewrite {1 5}(union_difference_L {[i]} (nclose N)) ?tl_tokens_union; try set_solver.
iDestruct "Htoks" as "[[Htoki Htoks0] Htoks1]". iFrame "Htoks0 Htoks1".
iInv tlN as "[[HP >Hdis]|>Htoki2]" "Hclose".
- iVs ("Hclose" with "[Htoki]") as "_". auto. 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