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

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