From 7d2b0a2883dba21999167c9d274629a316f8a293 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 15 Sep 2016 23:52:46 +0200
Subject: [PATCH] [from_exist_later] for instantiating an existential behind a
 later.

---
 proofmode/class_instances.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index aba0e60c1..753eec0ac 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) Φ.
-- 
GitLab