simp at *
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
γ : List Program
left✝ : γ ≠ ε
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
this✝ : ¬evaluate M w (⌈⌈γ ++ [∗β]⌉⌉ψ)
this : evaluate M w (~⌈β⌉⌈∗β⌉ψ)
⊢ evaluate M w (~⌈∗β⌉ψ)
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
γ : List Program
left✝ : ¬γ = []
Fγ_in : (Fs, γ) ∈ H β
hyp : ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, γ ++ [∗β]) ∈ l
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈γ ++ [∗β]⌉⌉ψ) → evaluate M w f
this✝ : ¬evaluate M w (⌈⌈γ ++ [∗β]⌉⌉ψ)
this : ∃ x, relate M β w x ∧ ∃ x_1, Relation.ReflTransGen (relate M β) x x_1 ∧ ¬evaluate M x_1 ψ
⊢ ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ