simp [modelCanSemImplyForm, evaluatePoint] at *
case mp
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
⊢ (M, v)⊨(~⌈⌈δ⌉⌉ξ) → Nonempty (witness M v δ ξ)
case mp
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
⊢ ¬evaluate M v (⌈⌈δ⌉⌉ξ) → Nonempty (witness M v δ ξ)