ex_intro1: ∀x:A. P x → Ex1 A P.
interpretation "exists1" 'exists x = (Ex1 ? x).
interpretation "exists" 'exists x = (Ex ? x).
ex_intro1: ∀x:A. P x → Ex1 A P.
interpretation "exists1" 'exists x = (Ex1 ? x).
interpretation "exists" 'exists x = (Ex ? x).