diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index aba0e60c19acb10062295aa0ec48af5d65d25ffd..753eec0ac5f730ab00c9d05e742a4d8a7320b062 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -320,6 +320,9 @@ Global Instance from_exist_rvs {A} P (Φ : A → uPred M) :
 Proof.
   rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
 Qed.
+Global Instance from_exist_later {A} P (Φ : A → uPred M) :
+  FromExist P Φ → FromExist (▷ P) (λ a, ▷ (Φ a))%I.
+Proof. rewrite /FromExist=> <-. apply exist_elim=>x. apply later_mono, exist_intro. Qed.
 
 (* IntoExist *)
 Global Instance into_exist_exist {A} (Φ : A → uPred M) : IntoExist (∃ a, Φ a) Φ.