specialize X_Y W M w v_X
case intro.intro.intro
X Y : List Formula
X_Y : X⊨Y
W : Type
M : KripkeModel W
w : W
v_X : ∀ φ ∈ X, evaluate M w φ
⊢ satisfiable Y
case intro.intro.intro
X Y : List Formula
W : Type
M : KripkeModel W
w : W
v_X : ∀ φ ∈ X, evaluate M w φ
X_Y : ∀ ψ ∈ Y, evaluate M w ψ
⊢ satisfiable Y