diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 214b3dc3b0492f0c65e36ab119871a7f8c5f687f..df0bcffb5de3d0db67c690cf0b9f14e717291c9a 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -615,6 +615,20 @@ Proof.
   by rewrite assoc (comm _ P1) -assoc wand_elim_r.
 Qed.
 
+Global Instance frame_impl_persistent R P1 P2 Q2 :
+  Frame true R P2 Q2 → Frame true R (P1 → P2) (P1 → Q2).
+Proof.
+  rewrite /Frame /==> ?. apply impl_intro_l.
+  by rewrite -and_sep_l assoc (comm _ P1) -assoc impl_elim_r and_sep_l.
+Qed.
+Global Instance frame_impl R P1 P2 Q2 :
+  Persistent P1 →
+  Frame false R P2 Q2 → Frame false R (P1 → P2) (P1 → Q2).
+Proof.
+  rewrite /Frame /==> ??. apply impl_intro_l.
+  by rewrite and_sep_l assoc (comm _ P1) -assoc -(and_sep_l P1) impl_elim_r.
+Qed.
+
 Class MakeLater (P lP : uPred M) := make_later : ▷ P ⊣⊢ lP.
 Global Instance make_later_true : MakeLater True True.
 Proof. by rewrite /MakeLater later_True. Qed.