diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index 8d3663167c6794fbf97a4a77995b1ac901cec7b1..ba5de9b212160f408d7fa0d49f14e3e74a26d227 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -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.