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