intro f f_in
case h.right
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈ε⌉⌉⌈β⌉ψ) → evaluate M w f
claim : ∀ (f : Formula), f ∈ Gs ∨ f = (~⌈⌈γ⌉⌉ψ) → evaluate M w f
⊢ ∀ (f : Formula), (f ∈ Fs ∨ f ∈ Gs) ∨ f = (~⌈⌈γ⌉⌉ψ) → evaluate M w f
case h.right
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈ε⌉⌉⌈β⌉ψ) → evaluate M w f
claim : ∀ (f : Formula), f ∈ Gs ∨ f = (~⌈⌈γ⌉⌉ψ) → evaluate M w f
f : Formula
f_in : (f ∈ Fs ∨ f ∈ Gs) ∨ f = (~⌈⌈γ⌉⌉ψ)
⊢ evaluate M w f