Theorem: quantifier_switch (BrownCs22/Demos/01-intro.lean)

State before:
p q r : Prop
P : ℕ → Prop
⊢ (¬∃ x, P x) → ∀ (x : ℕ), ¬P x
Tactic:
sorry
State after:
no goals