all_goals use W, M, w
case mp.intro.intro.intro
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
⊢ Satisfiable (X ∪ {φ})

case mpr.intro.intro.intro
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
⊢ Satisfiable (X ∪ {~~φ})
case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1
⊢ ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1

case h
X : Finset Formula
φ : Formula
W : Type
M : KripkeModel W
w : W
satX : ∀ φ_1 ∈ X ∪ {φ}, Evaluate (M, w) φ_1
⊢ ∀ φ_1 ∈ X ∪ {~~φ}, Evaluate (M, w) φ_1