diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index 4cf762d772d2c4519e702088fe58858dbd0eeeb2..8376ee688798102d13bdb1abc5a6b8a219ba3058 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -40,5 +40,14 @@ Section core.
 
   Lemma coreP_elim P : PersistentP P → coreP P -∗ P.
   Proof. rewrite /coreP. iIntros (?) "HCP". unshelve iApply ("HCP" $! P); auto. Qed.
-End core.
 
+  Lemma coreP_wand P Q :
+    (coreP P ⊢ Q) ↔ (P ⊢ □ Q).
+  Proof.
+    split.
+    - iIntros (HP) "HP". iDestruct (coreP_intro with "HP") as "#HcP".
+      iClear "∗". iAlways. by iApply HP.
+    - iIntros (HPQ) "HcP". iDestruct (coreP_mono _ _ HPQ with "HcP") as "HcQ".
+      iDestruct (coreP_elim with "HcQ") as "#HQ". done.
+  Qed.
+End core.