cases α
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) ξ)
case intro.intro.intro.atom_prog
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 ξ
a✝ : ℕ
v_α_w : relate M (·a✝) v w
⊢ Nonempty (witness M v ((·a✝) :: γs) ξ)

case intro.intro.intro.sequence
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 ξ
a✝¹ a✝ : Program
v_α_w : relate M (a✝¹;'a✝) v w
⊢ Nonempty (witness M v ((a✝¹;'a✝) :: γs) ξ)

case intro.intro.intro.union
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 ξ
a✝¹ a✝ : Program
v_α_w : relate M (a✝¹⋓a✝) v w
⊢ Nonempty (witness M v ((a✝¹⋓a✝) :: γs) ξ)

case intro.intro.intro.star
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 ξ
a✝ : Program
v_α_w : relate M (∗a✝) v w
⊢ Nonempty (witness M v ((∗a✝) :: γs) ξ)

case intro.intro.intro.test
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 ξ
a✝ : Formula
v_α_w : relate M (?'a✝) v w
⊢ Nonempty (witness M v ((?'a✝) :: γs) ξ)