intro v δ ξ wit def_n
W : Type
M : KripkeModel W
⊢ ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = 0 → evaluate M v (~⌈⌈δ⌉⌉ξ)
W : Type
M : KripkeModel W
v : W
δ : List Program
ξ : Formula
wit : witness M v δ ξ
def_n : wit.length = 0
⊢ evaluate M v (~⌈⌈δ⌉⌉ξ)