haveI := Classical.decEq
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
u : Finset F
hu : ↑u ⊆ ⋃ s, T s
⊢ ∃ s, ↑u ⊆ T s
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
u : Finset F
hu : ↑u ⊆ ⋃ s, T s
this : (α : Sort ?u.87136) → DecidableEq α
⊢ ∃ s, ↑u ⊆ T s