tauto
case intro.intro.intro
X : Finset Formula
φ : Formula
phi_in : φ ∈ X
notPhi_in : ~φ ∈ X
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, Evaluate (M, w) φ
this✝ : Evaluate (M, w) φ
this : Evaluate (M, w) (~φ)
⊢ False
no goals