constructor
case h
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_f : evaluate M w (Con (g (a, b) φ))
⊢ (∃ a_1 b_1, (a_1, b_1) ∈ X ∧ g (a_1, b_1) φ = g (a, b) φ) ∧ ∀ f ∈ g (a, b) φ, evaluate M w f
case h.left
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_f : evaluate M w (Con (g (a, b) φ))
⊢ ∃ a_1 b_1, (a_1, b_1) ∈ X ∧ g (a_1, b_1) φ = g (a, b) φ

case h.right
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_f : evaluate M w (Con (g (a, b) φ))
⊢ ∀ f ∈ g (a, b) φ, evaluate M w f