case zero =>
  intro v δ ξ wit def_n
  subst_eqs
  cases wit
  case nil =>
    subst_eqs
    simp [Formula.boxes, evaluate] at *
    assumption
  all_goals
    exfalso
    simp [witness.length] at *
W : Type
M : KripkeModel W
⊢ ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = 0 → evaluate M v (~⌈⌈δ⌉⌉ξ)
no goals