apply Iff.intro
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
⊢ Imp p (_root_.Exists q) ↔ ∃ a, p → q a
case mp
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
⊢ Imp p (_root_.Exists q) → ∃ a, p → q a

case mpr
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
⊢ (∃ a, p → q a) → Imp p (_root_.Exists q)