Commit 7d2b0a28 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

[from_exist_later] for instantiating an existential behind a later.

parent 4dda9d08
......@@ -320,6 +320,9 @@ Global Instance from_exist_rvs {A} P (Φ : A → uPred M) :
rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
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) Φ.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment