specialize w_Con f
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, []) ∈ H α
aaa : List Formula
_in_Hβ : (aaa, δ) ∈ H β
f : Formula
f_in : f ∈ Gs
w_Con : ∀ (f : Formula), (f ∈ Gs ∨ f ∈ aaa) ∨ f = (~⌈⌈δ⌉⌉ψ) → evaluate M w f
⊢ evaluate M w f
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, []) ∈ H α
aaa : List Formula
_in_Hβ : (aaa, δ) ∈ H β
f : Formula
f_in : f ∈ Gs
w_Con : (f ∈ Gs ∨ f ∈ aaa) ∨ f = (~⌈⌈δ⌉⌉ψ) → evaluate M w f
⊢ evaluate M w f