specialize w_sat_Z f f_in_Z
case intro.intro
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
Z : List Formula
w_sat_Z : ∀ f ∈ Z, evaluate M w f
Z_in_XS : Z ∈ XS
f : Formula
f_in_Z : f ∈ Z
w_not_f : ¬evaluate M w f
⊢ ∃ Y ∈ YS, ∀ f ∈ Y, evaluate M w f
case intro.intro
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
Z : List Formula
Z_in_XS : Z ∈ XS
f : Formula
f_in_Z : f ∈ Z
w_not_f : ¬evaluate M w f
w_sat_Z : evaluate M w f
⊢ ∃ Y ∈ YS, ∀ f ∈ Y, evaluate M w f