exists w
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
T : Sort u_1
P Q : T → Prop
equiv : ∀ (t : T), Q t ↔ P t
ex_t : ∃ t, P t
w : T
h : (fun t => P t) w
⊢ ∃ t, Q t
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
T : Sort u_1
P Q : T → Prop
equiv : ∀ (t : T), Q t ↔ P t
ex_t : ∃ t, P t
w : T
h : (fun t => P t) w
⊢ Q w