rcases satX with ⟨W,M,w,v_X⟩
X Y : List Formula
X_Y : X⊨Y
satX : satisfiable X
⊢ satisfiable Y
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