rcases lhs with ⟨Z, Z_in, w_sat_Z⟩
case mp
XS YS : List (List Formula)
W : Type
M : KripkeModel W
w : W
lhs : ∃ Y, (Y ∈ XS ∨ Y ∈ YS) ∧ ∀ f ∈ Y, Evaluate (M, w) f
⊢ (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f
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
⊢ (¬∃ Y ∈ XS, ∀ f ∈ Y, Evaluate (M, w) f) → ∃ Y ∈ YS, ∀ f ∈ Y, Evaluate (M, w) f