have := existsWitnessPath_ltr M v δ ξ
case mp
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
⊢ ¬evaluate M v (⌈⌈δ⌉⌉ξ) → Nonempty (witness M v δ ξ)
case mp
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
this : evaluate M v (~⌈⌈δ⌉⌉ξ) → Nonempty (witness M v δ ξ)
⊢ ¬evaluate M v (⌈⌈δ⌉⌉ξ) → Nonempty (witness M v δ ξ)