rcases rhs with ⟨Y, Y_in, satY⟩
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
nothyp : ¬∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
rhs : ∃ Y ∈ YS, ∀ 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
nothyp : ¬∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f
Y : List Formula
Y_in : Y ∈ YS
satY : ∀ f ∈ Y, evaluate M w f
⊢ ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, evaluate M w f