subst_eqs
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
ξ : Formula
a✝ : evaluate M v (~ξ)
def_n : (witness.nil a✝).length = n + 1
⊢ False
no goals