diff --git a/theories/bi/lib/core.v b/theories/bi/lib/core.v
index 3ad3caa5dbb4f1d7f5a32574190436b294636bd2..ce4ab4647a0cb1b2f0f39f36fd67e7f91bfcc4c7 100644
--- a/theories/bi/lib/core.v
+++ b/theories/bi/lib/core.v
@@ -7,7 +7,9 @@ Import bi.
     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.
+  (* TODO: Looks like we want notation for affinely-plainly; that lets us avoid
+  using conjunction/implication here. *)
+  (∀ Q : PROP, <affine> ■ (Q -∗ <pers> Q) -∗ <affine> ■ (P -∗ Q) -∗ Q)%I.
 Instance: Params (@coreP) 1.
 Typeclasses Opaque coreP.
 
@@ -16,14 +18,20 @@ Section core.
   Implicit Types P Q : PROP.
 
   Lemma coreP_intro P : P -∗ coreP P.
-  Proof. rewrite /coreP. iIntros "HP" (Q) "_ #HPQ". by iApply "HPQ". Qed.
+  Proof.
+    rewrite /coreP. iIntros "HP" (Q) "_ HPQ".
+    (* FIXME: Cannot apply HPQ directly. This works if we move it to the
+    persistent context, but why should we? *)
+    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". by iApply ("HC" with "[#] [#]").
+    iApply persistently_wand_affinely_plainly. iIntros "#HQ".
+    iApply persistently_wand_affinely_plainly. iIntros "#HPQ".
+    iApply "HQ". iApply "HC"; auto.
   Qed.
 
   Global Instance coreP_ne : NonExpansive (coreP (PROP:=PROP)).
@@ -35,7 +43,7 @@ Section core.
   Proof. solve_proper. Qed.
 
   Lemma coreP_elim P : Persistent P → coreP P -∗ P.
-  Proof. rewrite /coreP. iIntros (?) "HCP". iApply ("HCP" with "[#] [#]"); auto. Qed.
+  Proof. rewrite /coreP. iIntros (?) "HCP". iApply "HCP"; auto. Qed.
 
   (* TODO: Can we generalize this to non-affine BIs? *)
   Lemma coreP_wand `{!BiAffine PROP} P Q : (coreP P ⊢ Q) ↔ (P ⊢ <pers> Q).
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 7c58ce313a6f4ebf537464acf7f9920948bb7394..c897f5dfa4b2b761108067a6d55dda348dcb212f 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -419,4 +419,8 @@ Qed.
 Lemma test_iAssumption_False_no_loop : ∃ R, R ⊢ ∀ P, P.
 Proof. eexists. iIntros "?" (P). done. Qed.
 
+Lemma test_apply_affine_impl `{!BiPlainly PROP} (P : PROP) :
+  P -∗ (∀ Q : PROP, ■ (Q -∗ <pers> Q) → ■ (P -∗ Q) → Q).
+Proof. iIntros "HP" (Q) "_ #HPQ". by iApply "HPQ". Qed.
+
 End tests.