intro f f_in
case h.right.intro.refl.refl
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : evaluate M w (Con (Yset (Gs ∪ aaa, δ) ψ))
_in_Hβ : (aaa, δ) ∈ H β
⊢ ∀ (f : Formula), f ∈ Gs ∨ f = (~⌈β⌉ψ) → evaluate M w f
case h.right.intro.refl.refl
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
δ : List Program
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
aaa : List Formula
w_Con : evaluate M w (Con (Yset (Gs ∪ aaa, δ) ψ))
_in_Hβ : (aaa, δ) ∈ H β
f : Formula
f_in : f ∈ Gs ∨ f = (~⌈β⌉ψ)
⊢ evaluate M w f