diff --git a/_CoqProject b/_CoqProject
index e7841b5a09a85c12aca08a8f39aef49b342e92f5..6c5d46a4715d1f165af6de24a0959c09c81166ae 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -84,6 +84,7 @@ theories/base_logic/lib/cancelable_invariants.v
 theories/base_logic/lib/counter_examples.v
 theories/base_logic/lib/fractional.v
 theories/base_logic/lib/gen_heap.v
+theories/base_logic/lib/core.v
 theories/program_logic/adequacy.v
 theories/program_logic/lifting.v
 theories/program_logic/weakestpre.v
diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
new file mode 100644
index 0000000000000000000000000000000000000000..910cbee7a235c02e1963179b5469c8555e3e4bb7
--- /dev/null
+++ b/theories/base_logic/lib/core.v
@@ -0,0 +1,39 @@
+From iris.base_logic Require Import base_logic.
+From iris.proofmode Require Import tactics.
+Import uPred.
+
+(** The "core" of an assertion is its maximal persistent part.
+    It can be defined entirely within the logic... at least
+    in the shallow embedding. *)
+
+Definition coreP {M : ucmraT} (P : uPred M) : uPred M :=
+  (∀ (Q : uPred M) `(!PersistentP Q, !P -∗ Q), Q)%I.
+
+Section core.
+  Context {M : ucmraT}.
+  Implicit Types P Q : uPred M.
+
+  Lemma coreP_intro P :
+    P -∗ coreP P.
+  Proof.
+    iIntros "HP". iIntros (Q HQ HPQ). by iApply HPQ.
+  Qed.
+
+  Global Instance coreP_persistent P :
+    PersistentP (coreP P).
+  Proof.
+    iIntros "HCP". iApply always_forall. iIntros (Q).
+    iApply always_forall. iIntros (HQ). iApply always_forall.
+    iIntros (HPQ). iApply HQ. unshelve iApply ("HCP" $! Q). done.
+  Qed.
+
+  Lemma corP_elim P :
+    PersistentP P → coreP P -∗ P.
+  Proof.
+    iIntros (?) "HCP". unshelve iApply ("HCP" $! P).
+    iIntros "P". done.
+  Qed.
+End core.
+
+
+