simp_all [conEval, Yset, boxes_append]
case intro.intro.intro
ψ : 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 (⌈⌈γ ++ [∗β]⌉⌉ψ)
IHβ : evaluate M w (~⌈β⌉⌈∗β⌉ψ) ↔ ∃ Fδ ∈ H β, evaluate M w (Con (Yset Fδ (⌈∗β⌉ψ)))
⊢ evaluate M w (Con (Yset (Fs, γ) (⌈∗β⌉ψ)))
no goals