diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 9d152c84b5dea7a605a2b18933a78fd5414edcec..cdecce17dc9b8a3d6f0db94b2db15db0a9cf8da9 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -1004,14 +1004,15 @@ Qed.
 (* Plain *)
 Global Instance pure_plain φ : PlainP (⌜φ⌝ : uPred M)%I.
 Proof. by rewrite /PlainP plainly_pure. Qed.
-Global Instance pure_impl_plain φ Q : PlainP Q → PlainP (⌜φ⌝ → Q)%I.
+Global Instance impl_plain P Q : PlainP P → PlainP Q → PlainP (P → Q).
 Proof.
-  rewrite /PlainP pure_impl_forall plainly_forall. auto using forall_mono.
+  rewrite /PlainP=> HP HQ.
+  by rewrite {2}HP -plainly_impl_plainly -HQ plainly_elim.
 Qed.
-Global Instance pure_wand_plain φ Q : PlainP Q → PlainP (⌜φ⌝ -∗ Q)%I.
+Global Instance wand_plain P Q : PlainP P → PlainP Q → PlainP (P -∗ Q)%I.
 Proof.
-  rewrite /PlainP -always_impl_wand pure_impl_forall plainly_forall.
-  auto using forall_mono.
+  rewrite /PlainP=> HP HQ.
+  by rewrite {2}HP -{1}(plainly_elim P) !wand_impl_plainly -plainly_impl_plainly -HQ.
 Qed.
 Global Instance plainly_plain P : PlainP (☃ P).
 Proof. by intros; apply plainly_intro'. Qed.
@@ -1051,16 +1052,17 @@ Proof. destruct mx; apply _. Qed.
 (* Persistence *)
 Global Instance pure_persistent φ : PersistentP (⌜φ⌝ : uPred M)%I.
 Proof. by rewrite /PersistentP always_pure. Qed.
-Global Instance pure_impl_persistent φ Q :
-  PersistentP Q → PersistentP (⌜φ⌝ → Q)%I.
+Global Instance impl_persistent P Q :
+  PlainP P → PersistentP Q → PersistentP (P → Q).
 Proof.
-  rewrite /PersistentP pure_impl_forall always_forall. auto using forall_mono.
+  rewrite /PlainP /PersistentP=> HP HQ.
+  rewrite {2}HP -always_impl_plainly. by rewrite -HQ plainly_elim.
 Qed.
-Global Instance pure_wand_persistent φ Q :
-  PersistentP Q → PersistentP (⌜φ⌝ -∗ Q)%I.
+Global Instance wand_persistent P Q :
+  PlainP P → PersistentP Q → PersistentP (P -∗ Q)%I.
 Proof.
-  rewrite /PersistentP -always_impl_wand pure_impl_forall always_forall.
-  auto using forall_mono.
+  rewrite /PlainP /PersistentP=> HP HQ.
+  by rewrite {2}HP -{1}(plainly_elim P) !wand_impl_plainly -always_impl_plainly -HQ.
 Qed.
 Global Instance plainly_persistent P : PersistentP (☃ P).
 Proof. by rewrite /PersistentP always_plainly. Qed.
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 98a50e054c89c018dcb28424f34ecd329c8bd1d2..00389a413f29e736e66768af539f0da355794e71 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -480,6 +480,20 @@ Proof.
   by rewrite cmra_core_l cmra_core_idemp.
 Qed.
 
+Lemma always_impl_plainly P Q : (☃ P → □ Q) ⊢ □ (☃ P → Q).
+Proof.
+  unseal; split=> /= n x ? HPQ n' x' ????.
+  eapply uPred_mono with (core x), cmra_included_includedN; auto.
+  apply (HPQ n' x); eauto using cmra_validN_le.
+Qed.
+
+Lemma plainly_impl_plainly P Q : (☃ P → ☃ Q) ⊢ ☃ (☃ P → Q).
+Proof.
+  unseal; split=> /= n x ? HPQ n' x' ????.
+  eapply uPred_mono with ε, cmra_included_includedN; auto.
+  apply (HPQ n' x); eauto using cmra_validN_le.
+Qed.
+
 (* Later *)
 Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
 Proof.