no goals
ι : Type ?u.27917
ι' : Type ?u.27920
α : Type u_1
β : Type ?u.27926
γ : Type ?u.27929
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
p : α → Prop
⊢ (∀ (i : α), True → ∃ x, x ∈ Ici i ∧ p x) ↔ ∀ (a : α), ∃ b, b ≥ a ∧ p b
simp