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