use W, M, w
case intro.intro.intro.intro
X : Finset Formula
l : List Formula
W : Type
M : KripkeModel W
w : W
lNotSat : ∀ a ∈ l, ¬Evaluate (M, w) a
XSat : ∀ a ∈ X, Evaluate (M, w) a
φ : Formula
inl : φ ∈ l
⊢ ∃ W M w, ¬Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a
case h
X : Finset Formula
l : List Formula
W : Type
M : KripkeModel W
w : W
lNotSat : ∀ a ∈ l, ¬Evaluate (M, w) a
XSat : ∀ a ∈ X, Evaluate (M, w) a
φ : Formula
inl : φ ∈ l
⊢ ¬Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a