suffices goal : (~⌈∗β⌉ψ) ≡ ρ by
  have := @equiv_iff _ _ goal W M w
  simp only [modelCanSemImplyForm, evaluatePoint] at this
  rw [this]
ψ : Formula
W : Type
M : KripkeModel W
w : W
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
⊢ evaluate M w (~⌈∗β⌉ψ) ↔ evaluate M w (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 (∗β)))
⊢ (~⌈∗β⌉ψ)≡ρ