rcases hyp with ⟨W, M, w, w_⟩
case mpr
X : List Formula
φ : Formula
X_φ : X⊨[φ]
hyp : ∃ W M w, ∀ φ_1 ∈ X ∪ [~φ], evaluate M w φ_1
⊢ False
case mpr.intro.intro.intro
X : List Formula
φ : Formula
X_φ : X⊨[φ]
W : Type
M : KripkeModel W
w : W
w_ : ∀ φ_1 ∈ X ∪ [~φ], evaluate M w φ_1
⊢ False