diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index c435191f90e0d20374e77fbfb0e81aa157676a7c..522129ea0f42f1add98cba781b0faa408b9be9ee 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -124,6 +124,9 @@ Proof.
   rewrite -Hx. apply pure_intro. done.
 Qed.
 
+Global Instance from_pure_later P φ : FromPure P φ → FromPure (▷ P)%I φ.
+Proof. rewrite /FromPure=> ->. apply later_intro. Qed.
+
 (* IntoPersistentP *)
 Global Instance into_persistentP_always_trans P Q :
   IntoPersistentP P Q → IntoPersistentP (□ P) Q | 0.