simp only [evaluate, witness.length, Formula.boxes, relate, not_forall, exists_prop] at *
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
Fε_in_Hα : (Fs, ε) ∈ H α
v_Fs : evaluate M v (Con Fs)
wit_γs : witness M v γs ξ
def_n : (witness.consEmpty Fs Fε_in_Hα v_Fs wit_γs).length = n + 1
⊢ evaluate M v (~⌈⌈α :: γs⌉⌉ξ)
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
γs : List Program
Fs : List Formula
Fε_in_Hα : (Fs, ε) ∈ H α
v_Fs : evaluate M v (Con Fs)
wit_γs : witness M v γs ξ
def_n : 1 + wit_γs.length = n + 1
IH : ∀ (v : W) (δ : List Program) (ξ : Formula) (wit : witness M v δ ξ), wit.length = n → ¬evaluate M v (⌈⌈δ⌉⌉ξ)
⊢ ∃ x, relate M α v x ∧ ¬evaluate M x (⌈⌈γs⌉⌉ξ)