simp_all
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
no goals