diff --git a/_CoqProject b/_CoqProject
index 4ddfcad2828c5bac0ccd3d904367d4bc1cd0b650..50d4739448a691c727ca1a0361e3da48871181eb 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -39,6 +39,7 @@ theories/bi/monpred.v
 theories/bi/embedding.v
 theories/bi/lib/fractional.v
 theories/bi/lib/atomic.v
+theories/bi/lib/core.v
 theories/base_logic/upred.v
 theories/base_logic/derived.v
 theories/base_logic/base_logic.v
@@ -58,7 +59,6 @@ theories/base_logic/lib/boxes.v
 theories/base_logic/lib/na_invariants.v
 theories/base_logic/lib/cancelable_invariants.v
 theories/base_logic/lib/gen_heap.v
-theories/base_logic/lib/core.v
 theories/base_logic/lib/fancy_updates_from_vs.v
 theories/program_logic/adequacy.v
 theories/program_logic/lifting.v
diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
deleted file mode 100644
index f64ad81cfac2220e4dc1ed4635e40243f4f1e2af..0000000000000000000000000000000000000000
--- a/theories/base_logic/lib/core.v
+++ /dev/null
@@ -1,45 +0,0 @@
-From iris.base_logic Require Import base_logic.
-From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
-Import uPred.
-
-(** The "core" of an assertion is its maximal persistent part,
-    i.e. the conjunction of all persistent assertions that are weaker
-    than P (as in, implied by P). *)
-Definition coreP {M : ucmraT} (P : uPred M) : uPred M :=
-  (∀ Q, ■ (P → □ Q) → □ Q)%I.
-Instance: Params (@coreP) 1.
-Typeclasses Opaque coreP.
-
-Section core.
-  Context {M : ucmraT}.
-  Implicit Types P Q : uPred M.
-
-  Lemma coreP_intro P : P -∗ coreP P.
-  Proof. rewrite /coreP. iIntros "HP" (Q) "HPQ". by iApply "HPQ". Qed.
-
-  Global Instance coreP_persistent P : Persistent (coreP P).
-  Proof. rewrite /coreP /Persistent. iIntros "#HC" (Q) "!#". iApply "HC". Qed.
-
-  Global Instance coreP_ne : NonExpansive (@coreP M).
-  Proof. solve_proper. Qed.
-  Global Instance coreP_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@coreP M).
-  Proof. solve_proper. Qed.
-
-  Global Instance coreP_mono : Proper ((⊢) ==> (⊢)) (@coreP M).
-  Proof. solve_proper. Qed.
-
-  Lemma coreP_elim P : Persistent P → coreP P -∗ P.
-  Proof.
-    rewrite /coreP. iIntros (?) "HCP". iApply ("HCP" $! P with "[]"). auto.
-  Qed.
-
-  Lemma coreP_wand P Q : (coreP P ⊢ Q) ↔ (P ⊢ □ Q).
-  Proof.
-    split.
-    - iIntros (HP) "HP". iDestruct (coreP_intro with "HP") as "#HcP".
-      iAlways. by iApply HP.
-    - iIntros (HPQ) "HcP". iDestruct (coreP_mono _ _ HPQ with "HcP") as "HcQ".
-      by iDestruct (coreP_elim with "HcQ") as "#HQ".
-  Qed.
-End core.
diff --git a/theories/bi/lib/core.v b/theories/bi/lib/core.v
new file mode 100644
index 0000000000000000000000000000000000000000..cdd8ee50238082e9030d653292a04f155ca69266
--- /dev/null
+++ b/theories/bi/lib/core.v
@@ -0,0 +1,66 @@
+From iris.bi Require Export bi plainly.
+From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
+Import bi.
+
+(** The "core" of an assertion is its maximal persistent part,
+    i.e. the conjunction of all persistent assertions that are weaker
+    than P (as in, implied by P). *)
+Definition coreP `{!BiPlainly PROP} (P : PROP) : PROP :=
+  (∀ Q : PROP, ■ (Q -∗ <pers> Q) → ■ (P -∗ Q) → Q)%I.
+Instance: Params (@coreP) 1.
+Typeclasses Opaque coreP.
+
+Section core.
+  Context `{!BiPlainly PROP}.
+  Implicit Types P Q : PROP.
+
+  Lemma coreP_intro P : P -∗ coreP P.
+  Proof.
+    rewrite /coreP. iIntros "HP" (Q) "_ HPQ".
+    (* FIXME: Cannot apply HPQ directly. *)
+    iDestruct (affinely_plainly_elim with "HPQ") as "HPQ".
+    by iApply "HPQ".
+  Qed.
+
+  Global Instance coreP_persistent P : Persistent (coreP P).
+  Proof.
+    rewrite /coreP /Persistent. iIntros "HC" (Q).
+    iApply persistently_impl_plainly. iIntros "#HQ".
+    iApply persistently_impl_plainly. iIntros "#HPQ".
+    iApply "HQ".
+    (* FIXME: [iApply "HC"] should work. *)
+    iSpecialize ("HC" with "HQ"). iSpecialize ("HC" with "HPQ"). done.
+  Qed.
+
+  Global Instance coreP_ne : NonExpansive (coreP (PROP:=PROP)).
+  Proof. solve_proper. Qed.
+  Global Instance coreP_proper : Proper ((⊣⊢) ==> (⊣⊢)) (coreP (PROP:=PROP)).
+  Proof. solve_proper. Qed.
+
+  Global Instance coreP_mono : Proper ((⊢) ==> (⊢)) (coreP (PROP:=PROP)).
+  Proof. solve_proper. Qed.
+
+  Lemma coreP_elim P : Persistent P → coreP P -∗ P.
+  Proof.
+    rewrite /coreP. iIntros (?) "HCP". iSpecialize ("HCP" $! P).
+    (* FIXME: [iApply "HCP"] should work. *)
+    iAssert (■ (P -∗ <pers> P))%I as "#HPpers".
+    { iModIntro. iApply persistent. }
+    iSpecialize ("HCP" with "HPpers").
+    iAssert (■ (P -∗ P))%I as "#HP".
+    { iIntros "!> HP". done. }
+    iSpecialize ("HCP" with "HP").
+    done.
+  Qed.
+
+  (* TODO: Can we generalize this to non-affine BIs? *)
+  Lemma coreP_wand `{!BiAffine PROP} P Q : (coreP P ⊢ Q) ↔ (P ⊢ <pers> Q).
+  Proof.
+    split.
+    - iIntros (HP) "HP". iDestruct (coreP_intro with "HP") as "#HcP".
+      iAlways. by iApply HP.
+    - iIntros (HPQ) "HcP". iDestruct (coreP_mono _ _ HPQ with "HcP") as "HcQ".
+      by iDestruct (coreP_elim with "HcQ") as "#HQ".
+  Qed.
+End core.
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index 7f63cc8bf3b77276d19f8575b44c5c78ad89cb86..756364c992b9641c7afe2d44f9768176a7679d36 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -1,4 +1,4 @@
-From iris.bi Require Export derived_laws.
+From iris.bi Require Import derived_laws.
 From iris.algebra Require Import monoid.
 Import interface.bi derived_laws.bi.