have : ∃ γ, δ = γ ++ [∗β] ∧ γ ≠ ε ∧ (Fs,γ) ∈ H β := by aesop
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
w_Con : ∀ f ∈ Yset (Fs, δ) ψ, evaluate M w f
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, δ) ∈ l
⊢ evaluate M w (~⌈∗β⌉ψ)
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
w_Con : ∀ f ∈ Yset (Fs, δ) ψ, evaluate M w f
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, δ) ∈ l
this : ∃ γ, δ = γ ++ [∗β] ∧ γ ≠ ε ∧ (Fs, γ) ∈ H β
⊢ evaluate M w (~⌈∗β⌉ψ)