subst def_fs
case mpr.intro.intro.intro.intro.intro
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
fs : List Formula
w_fs : ∀ f ∈ fs, evaluate M w f
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
def_fs : g (a, b) φ = fs
⊢ ∃ f, (∃ a b, (a, b) ∈ X ∧ Con (g (a, b) φ) = f) ∧ evaluate M w f
case mpr.intro.intro.intro.intro.intro
W : Type
X : List (List Formula × List Program)
M : KripkeModel W
w : W
φ : Formula
g : List Formula × List Program → Formula → List Formula
a : List Formula
b : List Program
ab_in : (a, b) ∈ X
w_fs : ∀ f ∈ g (a, b) φ, evaluate M w f
⊢ ∃ f, (∃ a b, (a, b) ∈ X ∧ Con (g (a, b) φ) = f) ∧ evaluate M w f