Commit 9b40c80d authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove useless lemma.

parent dc297188
...@@ -265,9 +265,4 @@ Section Rules. ...@@ -265,9 +265,4 @@ Section Rules.
iFrame "Hl". iIntros "Hl". iFrame "Hl". iIntros "Hl".
iApply stack_owns_close. by iFrame. iApply stack_owns_close. by iFrame.
Qed. Qed.
Lemma stack_owns_later_open_close h l v :
stack_owns h l ↦ˢᵗᵏ v
(l ↦ᵢ v (l ↦ᵢ v - (stack_owns h l ↦ˢᵗᵏ v))).
Proof. iIntros "H >". by iApply stack_owns_open_close. Qed.
End Rules. End Rules.
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