case inr hyp =>
  have : ∃ γ, δ = γ ++ [∗β] ∧ γ ≠ ε ∧ (Fs,γ) ∈ H β := by aesop
  rcases this with ⟨γ, ⟨δ_def, _, Fγ_in⟩⟩
  subst δ_def
  simp only [Yset, List.mem_union_iff, List.mem_singleton] at w_Con
  have := w_Con (~⌈⌈γ ++ [∗β]⌉⌉ψ)
  simp at this
  suffices evaluate M w (~⌈β⌉⌈∗β⌉ψ) by
    simp at *
    rcases this with ⟨v, ⟨w_β_v, ⟨u, ⟨v_Sβ_u, u_nPsi⟩⟩⟩⟩
    refine ⟨u, ?_, u_nPsi⟩
    exact Relation.ReflTransGen.head w_β_v v_Sβ_u
  have IHβ := localDiamondTruth β (⌈∗β⌉ψ) W M w
  rw [disEval, helper] at IHβ
  rw [IHβ]
  refine ⟨⟨Fs, γ⟩, ⟨Fγ_in, ?_⟩⟩
  simp_all [conEval, Yset, boxes_append]
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
w_Con : ∀ f ∈ Yset (Fs, δ) ψ, evaluate M w f
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, δ) ∈ l
⊢ evaluate M w (~⌈∗β⌉ψ)
no goals