by_contra
case mp
V : Type ?u.5314
inst✝ : SetTheory V
α : Sort u_1
p : α → Prop
⊢ (¬∀ (x : α), p x) → ∃ x, ¬p x
case mp
V : Type ?u.5314
inst✝ : SetTheory V
α : Sort u_1
p : α → Prop
x✝ : ¬((¬∀ (x : α), p x) → ∃ x, ¬p x)
⊢ False