rcases hyp with ⟨X, X_in, satX⟩
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
hyp : ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
⊢ ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, evaluate M w f
case intro.intro
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
X : List Formula
X_in : X ∈ XS
satX : ∀ f ∈ X, evaluate M w f
⊢ ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, evaluate M w f