case nil =>
  subst_eqs
  simp [Formula.boxes, evaluate] at *
  assumption
W : Type
M : KripkeModel W
v : W
ξ : Formula
a✝ : evaluate M v (~ξ)
def_n : (witness.nil a✝).length = 0
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ)
no goals