case consAtom a v1 γs v0_a_v1 wit_v1_γs =>
  simp only [evaluate, witness.length, Formula.boxes, relate, not_forall, exists_prop] at *
  refine ⟨v1, v0_a_v1, IH v1 γs ξ wit_v1_γs ?_⟩
  linarith
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
a : ℕ
v1 : W
γs : List Program
v0_a_v1 : M.Rel a v v1
wit_v1_γs : witness M v1 γs ξ
def_n : (witness.consAtom v0_a_v1 wit_v1_γs).length = n + 1
⊢ evaluate M v (~⌈⌈(·a) :: γs⌉⌉ξ)
no goals