simp at *
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
case mpr.intro.intro.intro.cons
φ : Formula
W : Type
M : KripkeModel W
w : W
head✝ : Formula
tail✝ : List Formula
w_ : evaluate M w head✝ ∧ ∀ (a : Formula), a ∈ tail✝ ∨ a = (~φ) → evaluate M w a
X_φ : evaluate M w head✝ → (∀ a ∈ tail✝, evaluate M w a) → evaluate M w φ
this : ¬evaluate M w φ
⊢ False