exact ⟨0, by simp⟩
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
hu : ↑∅ ⊆ ⋃ s, T s
⊢ ∃ s, ↑∅ ⊆ T s
no goals