cases em (γ = ε)
case mpr.intro.mk.intro.intro.intro.intro.intro.intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
w_Con : evaluate M w (Con (Yset (Fs, δ) ψ))
Gs : List Formula
γ : List Program
Gγ_in : (Gs, γ) ∈ H α
Gγ_in_l : (Fs, δ) ∈ if γ = [] then (List.map (fun x => [(Gs ∪ x.1, x.2)]) (H β)).join else [(Gs, γ ++ [β])]
⊢ ∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))
case mpr.intro.mk.intro.intro.intro.intro.intro.intro.inl
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
w_Con : evaluate M w (Con (Yset (Fs, δ) ψ))
Gs : List Formula
γ : List Program
Gγ_in : (Gs, γ) ∈ H α
Gγ_in_l : (Fs, δ) ∈ if γ = [] then (List.map (fun x => [(Gs ∪ x.1, x.2)]) (H β)).join else [(Gs, γ ++ [β])]
h✝ : γ = ε
⊢ ∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))

case mpr.intro.mk.intro.intro.intro.intro.intro.intro.inr
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
w_Con : evaluate M w (Con (Yset (Fs, δ) ψ))
Gs : List Formula
γ : List Program
Gγ_in : (Gs, γ) ∈ H α
Gγ_in_l : (Fs, δ) ∈ if γ = [] then (List.map (fun x => [(Gs ∪ x.1, x.2)]) (H β)).join else [(Gs, γ ++ [β])]
h✝ : ¬γ = ε
⊢ ∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))