case cons α γs IH =>
  intro v_
  simp at *
  rcases v_ with ⟨w, v_α_w, w_⟩
  rcases IH w w_ with ⟨w_wit⟩
  cases α case atom_prog a =>
    simp at v_α_w
    constructor
    apply witness.consAtom v_α_w w_wit
  case sequence α β =>
    simp at *
    rcases v_α_w with ⟨u, v_u, u_w⟩
    rcases IH w w_ with ⟨w_wit⟩
    constructor
    sorry
  case union α β =>
    constructor
    sorry
  case test τ =>
    constructor
    sorry
  case star β =>
    constructor
    sorry
W : Type
M : KripkeModel W
ξ : Formula
α : Program
γs : List Program
IH : ∀ (v : W), evaluate M v (~⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
v : W
⊢ evaluate M v (~⌈⌈α :: γs⌉⌉ξ) → Nonempty (witness M v (α :: γs) ξ)
no goals