Skip to content
Snippets Groups Projects
Commit fee229c1 authored by Ralf Jung's avatar Ralf Jung
Browse files

core: fix typo in lemma name

parent 0283ccbb
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/base_logic/lib/core.v
+ 1
− 1
View file @ fee229c1
......@@ -23,7 +23,7 @@ Section core.
iIntros (HPQ). iApply HQ. unshelve iApply ("HCP" $! Q). done.
Qed.
Lemma corP_elim P : PersistentP P → coreP P -∗ P.
Lemma coreP_elim P : PersistentP P → coreP P -∗ P.
Proof.
iIntros (?) "HCP". unshelve iApply ("HCP" $! P). iIntros "P". done.
Qed.
......
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