have claim : ∃ Gγ ∈ H β, evaluate M w (Con (Yset Gγ ψ)) := by
  rw [conEval] at w_Con
  simp [Yset, Con] at w_Con
  have := w_Con (~⌈β⌉ψ)
  simp only [or_true, forall_true_left] at this
  have IHβ := localDiamondTruth β ψ W M w
  rw [IHβ] at this
  rw [disEval, helper] at this
  exact this
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
⊢ ∃ Fδ ∈ H (α;'β), evaluate M w (Con (Yset Fδ ψ))
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
claim : ∃ Gγ ∈ H β, evaluate M w (Con (Yset Gγ ψ))
⊢ ∃ Fδ ∈ H (α;'β), evaluate M w (Con (Yset Fδ ψ))