diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 8bc2fbbc3fc61b34cdced692b7daa31c0652802f..9d152c84b5dea7a605a2b18933a78fd5414edcec 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -961,7 +961,7 @@ Global Instance limit_preserving_PlainP {A:ofeT} `{Cofe A} (Φ : A → uPred M)
   NonExpansive Φ → LimitPreserving (λ x, PlainP (Φ x)).
 Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
 
-Global Instance Plain_Persistent P : PlainP P → PersistentP P.
+Lemma plain_persistent P : PlainP P → PersistentP P.
 Proof. rewrite /PlainP /PersistentP => HP. by rewrite {1}HP plainly_elim'. Qed.
 
 Lemma plainly_plainly P `{!PlainP P} : ☃ P ⊣⊢ P.
@@ -1062,6 +1062,8 @@ Proof.
   rewrite /PersistentP -always_impl_wand pure_impl_forall always_forall.
   auto using forall_mono.
 Qed.
+Global Instance plainly_persistent P : PersistentP (☃ P).
+Proof. by rewrite /PersistentP always_plainly. Qed.
 Global Instance always_persistent P : PersistentP (â–¡ P).
 Proof. by intros; apply always_intro'. Qed.
 Global Instance and_persistent P Q :
@@ -1166,3 +1168,12 @@ Global Instance uPred_ownM_sep_homomorphism :
 Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
 End derived.
 End uPred.
+
+(* When declared as an actual instance, [plain_persistent] will give cause
+failing proof searches to take exponential time, as Coq will try to apply it
+the instance at any node in the proof search tree.
+
+To avoid that, we declare it using a [Hint Immediate], so that it will only be
+used at the leaves of the proof search tree, i.e. when the premise of the hint
+can be derived from just the current context. *)
+Hint Immediate uPred.plain_persistent : typeclass_instances.