rw [conEval] at w_Con
case intro.mk.intro
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H (∗β)
w_Con : evaluate M w (Con (Yset (Fs, δ) ψ))
⊢ evaluate M w (~⌈∗β⌉ψ)
case intro.mk.intro
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H (∗β)
w_Con : ∀ f ∈ Yset (Fs, δ) ψ, evaluate M w f
⊢ evaluate M w (~⌈∗β⌉ψ)