have right_to_left_claim : ∀ W M (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ) := by
  clear W M w; intro W M w
  unfold_let ρ
  rw [disEval, helper]
  rintro ⟨⟨Fs,δ⟩, ⟨Fδ_in, w_Con⟩⟩
  rw [conEval] at w_Con
  simp [H] at Fδ_in
  cases Fδ_in
  case inl hyp =>
    cases hyp
    subst_eqs
    simp_all [Yset]
    use w
  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
W : Type
M : KripkeModel W
w : W
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
⊢ (~⌈∗β⌉ψ)≡ρ
ψ : Formula
W : Type
M : KripkeModel W
w : W
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
⊢ (~⌈∗β⌉ψ)≡ρ