case inl hyp =>
  rcases hyp with ⟨X, X_in, satX⟩
  use X
  exact ⟨Or.inl 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
no goals