cases 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