have := w_ (~φ)
case mpr.intro.intro.intro.cons
φ : Formula
W : Type
M : KripkeModel W
w : W
head✝ : Formula
tail✝ : List Formula
w_ : ∀ φ_1 ∈ head✝ :: tail✝ ∪ [~φ], evaluate M w φ_1
X_φ : (∀ φ ∈ head✝ :: tail✝, evaluate M w φ) → ∀ ψ ∈ [φ], evaluate M w ψ
⊢ False
case mpr.intro.intro.intro.cons
φ : Formula
W : Type
M : KripkeModel W
w : W
head✝ : Formula
tail✝ : List Formula
w_ : ∀ φ_1 ∈ head✝ :: tail✝ ∪ [~φ], evaluate M w φ_1
X_φ : (∀ φ ∈ head✝ :: tail✝, evaluate M w φ) → ∀ ψ ∈ [φ], evaluate M w ψ
this : (~φ) ∈ head✝ :: tail✝ ∪ [~φ] → evaluate M w (~φ)
⊢ False