cases (Classical.em (∃ Y, Y ∈ XS ∧ ∀ (f : Formula), f ∈ Y → evaluate M w f))
case mpr
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
rhs : (¬∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f) → ∃ Y ∈ YS, ∀ f ∈ Y, evaluate M w f
⊢ ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, evaluate M w f
case mpr.inl
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
rhs : (¬∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f) → ∃ Y ∈ YS, ∀ f ∈ Y, evaluate M w f
h✝ : ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
⊢ ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, evaluate M w f

case mpr.inr
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
rhs : (¬∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f) → ∃ Y ∈ YS, ∀ f ∈ Y, evaluate M w f
h✝ : ¬∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
⊢ ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, evaluate M w f