diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index 6630d803a2bc315e3fd795277883eda227559417..d070516b97f2ffe3f4a9a10e880d250b21fffbc6 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -8,7 +8,7 @@ Import uPred.
     in the shallow embedding. *)
 
 Definition coreP {M : ucmraT} (P : uPred M) : uPred M :=
-  (∀ `(!PersistentP Q, P ⊢ Q), Q)%I.
+  (∀ `(!PersistentP Q), ⌜P ⊢ Q⌝ → Q)%I.
 Instance: Params (@coreP) 1.
 Typeclasses Opaque coreP.
 
@@ -25,7 +25,7 @@ Section core.
   Global Instance coreP_mono : Proper ((⊢) ==> (⊢)) (@coreP M).
   Proof.
     rewrite /coreP. iIntros (P P' ?) "H"; iIntros (Q ??).
-    unshelve iApply ("H" $! Q). by etrans.
+    iApply ("H" $! Q with "[%]"). by etrans.
   Qed.
 
   Global Instance coreP_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@coreP M).