intro nSat W M w satX
case mp
X : List Formula
φ : Formula
⊢ (∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), ∃ x_3 ∈ X ∪ [~φ], ¬evaluate x_1 x_2 x_3) → semImpliesLists X [φ]
case mp
X : List Formula
φ : Formula
nSat : ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), ∃ x_3 ∈ X ∪ [~φ], ¬evaluate x_1 x_2 x_3
W : Type
M : KripkeModel W
w : W
satX : ∀ φ ∈ X, evaluate M w φ
⊢ ∀ ψ ∈ [φ], evaluate M w ψ