case inl Z_in_XS =>
  specialize notL Z Z_in_XS
  rcases notL with ⟨f, f_in_Z, w_not_f⟩
  specialize w_sat_Z f f_in_Z
  absurd w_sat_Z
  exact w_not_f
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
Z_in_XS : Z ∈ XS
⊢ ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
no goals