Rule. ex_intro
(H ⊢ P t) → (H ⊢ ∃x. P x)