simp [Formula.boxes, evaluate] at *
case refl
W : Type
M : KripkeModel W
v : W
ξ : Formula
a✝ : evaluate M v (~ξ)
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ)
case refl
W : Type
M : KripkeModel W
v : W
ξ : Formula
a✝ : ¬evaluate M v ξ
⊢ ¬evaluate M v ξ