cases Z_in
case mp.intro.intro
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
Z : List Formula
Z_in : Z ∈ XS ∨ Z ∈ YS
w_sat_Z : ∀ f ∈ Z, evaluate M w f
notL : ∀ x ∈ XS, ∃ x_1 ∈ x, ¬evaluate M w x_1
⊢ ∃ Y ∈ YS, ∀ f ∈ Y, evaluate M w f
case mp.intro.intro.inl
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
Z : List Formula
w_sat_Z : ∀ f ∈ Z, evaluate M w f
notL : ∀ x ∈ XS, ∃ x_1 ∈ x, ¬evaluate M w x_1
h✝ : Z ∈ XS
⊢ ∃ Y ∈ YS, ∀ f ∈ Y, evaluate M w f

case mp.intro.intro.inr
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
Z : List Formula
w_sat_Z : ∀ f ∈ Z, evaluate M w f
notL : ∀ x ∈ XS, ∃ x_1 ∈ x, ¬evaluate M w x_1
h✝ : Z ∈ YS
⊢ ∃ Y ∈ YS, ∀ f ∈ Y, evaluate M w f