apply satX
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' ∈ X
satX : φ' ∈ X ∪ {φ} → Evaluate (M, w) φ'
⊢ Evaluate (M, w) φ'
case h.inl
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
φ' : Formula
h✝ : φ' ∈ X
satX : φ' ∈ X ∪ {φ} → Evaluate (M, w) φ'
⊢ φ' ∈ X ∪ {φ}