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
Fs : List Formula
v1 : W
ηs γs : List Program
a : ℕ
Fsaηs_in_Hα : (Fs, (·a) :: ηs) ∈ H α
v_a_v1 : M.Rel a v v1
four : evaluate M v (Con Fs)
wit_v1_ηγs : witness M v1 (ηs ++ γs) ξ
def_n : (witness.consComp v_a_v1 Fsaηs_in_Hα four wit_v1_ηγs).length = n + 1
⊢ evaluate M v (~⌈⌈α :: γs⌉⌉ξ)
W : Type
M : KripkeModel W
n : ℕ
v : W
ξ : Formula
α : Program
Fs : List Formula
v1 : W
ηs γs : List Program
a : ℕ
Fsaηs_in_Hα : (Fs, (·a) :: ηs) ∈ H α
v_a_v1 : M.Rel a v v1
four : evaluate M v (Con Fs)
wit_v1_ηγs : witness M v1 (ηs ++ γs) ξ
def_n : 1 + wit_v1_ηγ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⌉⌉ξ)