rcases IH w w_ with ⟨w_wit⟩
case intro.intro
W : Type
M : KripkeModel W
ξ : Formula
α : Program
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
v_α_w : relate M α v w
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
⊢ Nonempty (witness M v (α :: γs) ξ)
case intro.intro.intro
W : Type
M : KripkeModel W
ξ : Formula
α : Program
γs : List Program
v : W
IH : ∀ (v : W), ¬evaluate M v (⌈⌈γs⌉⌉ξ) → Nonempty (witness M v γs ξ)
w : W
v_α_w : relate M α v w
w_ : ¬evaluate M w (⌈⌈γs⌉⌉ξ)
w_wit : witness M w γs ξ
⊢ Nonempty (witness M v (α :: γs) ξ)