diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index 844842a897de86773c3b0ff894b02abfb6108ef6..3421dccb1b4c07e8edb4010a2fc3f71ba984347f 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.