no goals
ι : Type ?u.35304
ι' : Type ?u.35307
α : Type u_1
β : Type ?u.35313
γ : Type ?u.35316
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : NoMaxOrder α
p : α → Prop
⊢ (∀ (i : α), True → ∃ x, x ∈ Ioi i ∧ p x) ↔ ∀ (a : α), ∃ b, b > a ∧ p b
simp