From 15e4ed53dc00ee90f9212d4a4ef75b499e158874 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 19 Jan 2019 16:28:04 +0000
Subject: [PATCH] Hoare existential rule

---
 theories/program_logic/hoare.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index 844842a89..3421dccb1 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -154,4 +154,9 @@ Proof.
   iIntros (?) "#Hwp !# [HP HR]".
   iApply wp_frame_step_r'; try done. iFrame "HR". by iApply "Hwp".
 Qed.
+
+Lemma ht_exists (T : Type) s E (P : T → iProp Σ) Φ e :
+  (∀ x, {{ P x }} e @ s; E {{ Φ }}) ⊢ {{ ∃ x, P x }} e @ s; E {{ Φ }}.
+Proof. iIntros "#HT !# HP". iDestruct "HP" as (x) "HP". by iApply "HT". Qed.
+
 End hoare.
-- 
GitLab