rw [disEval, helper] at this
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈β⌉ψ) → evaluate M w f
this : evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H β)))
IHβ : evaluate M w (~⌈β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H β)))
⊢ ∃ Gγ ∈ H β, evaluate M w (Con (Yset Gγ ψ))
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈β⌉ψ) → evaluate M w f
this : ∃ Fδ ∈ H β, evaluate M w (Con (Yset Fδ ψ))
IHβ : evaluate M w (~⌈β⌉ψ) ↔ evaluate M w (dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H β)))
⊢ ∃ Gγ ∈ H β, evaluate M w (Con (Yset Gγ ψ))