sorry
case intro.intro.intro.val
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
w_wit : witness M w γs ξ
⊢ witness M v ((α;'β) :: γs) ξ
no goals