cases wit
W : Type
M : KripkeModel W
n : ℕ
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → evaluate M v (~⌈⌈δ⌉⌉ξ)
v : W
δ : List Program
ξ : Formula
wit : witness M v δ ξ
def_n : wit.length = n + 1
⊢ evaluate M v (~⌈⌈δ⌉⌉ξ)
case nil
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
⊢ evaluate M v (~⌈⌈[]⌉⌉ξ)

case consAtom
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✝¹ : ℕ
v1✝ : W
γs✝ : List Program
v0_a_v1✝ : M.Rel a✝¹ v v1✝
a✝ : witness M v1✝ γs✝ ξ
def_n : (witness.consAtom v0_a_v1✝ a✝).length = n + 1
⊢ evaluate M v (~⌈⌈(·a✝¹) :: γs✝⌉⌉ξ)

case consEmpty
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
α✝ : Program
γs✝ : List Program
Fs✝ : List Formula
a✝² : (Fs✝, ε) ∈ H α✝
a✝¹ : evaluate M v (Con Fs✝)
a✝ : witness M v γs✝ ξ
def_n : (witness.consEmpty Fs✝ a✝² a✝¹ a✝).length = n + 1
⊢ evaluate M v (~⌈⌈α✝ :: γs✝⌉⌉ξ)

case consComp
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
α✝ : Program
Fs✝ : List Formula
v1✝ : W
ηs✝ γs✝ : List Program
a✝⁴ : ℕ
a✝³ : (Fs✝, (·a✝⁴) :: ηs✝) ∈ H α✝
a✝² : M.Rel a✝⁴ v v1✝
a✝¹ : evaluate M v (Con Fs✝)
a✝ : witness M v1✝ (ηs✝ ++ γs✝) ξ
def_n : (witness.consComp a✝² a✝³ a✝¹ a✝).length = n + 1
⊢ evaluate M v (~⌈⌈α✝ :: γs✝⌉⌉ξ)