simp [Yset, conEval, boxes_append] at *
case h.right
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, δ) (⌈β⌉ψ)))
δ_not_ε : ¬δ = ε
⊢ evaluate M w (Con (Yset (Fs, δ ++ [β]) ψ))
case h.right
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
δ_not_ε : ¬δ = []
w_Con : ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉⌈β⌉ψ) → evaluate M w f
⊢ ∀ (f : Formula), f ∈ Fs ∨ f = (~⌈⌈δ⌉⌉⌈β⌉ψ) → evaluate M w f