Commit 6d7bb44a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Revert "Remove useless lemma."

This reverts commit 9b40c80d.
parent 9b40c80d
...@@ -265,4 +265,9 @@ Section Rules. ...@@ -265,4 +265,9 @@ 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