simp [conEval, Xset]
case refine_3
α : Program
ℓ : TP α
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con (Xset α ℓ ψ)⋀signature α ℓ) ↔
    evaluate M w (Con (List.map (fun αs => ⌈⌈αs⌉⌉ψ) (P α ℓ))⋀signature α ℓ)
case refine_3
α : Program
ℓ : TP α
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (signature α ℓ) →
    ((∀ (f : Formula), (f ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉ψ) = f) → evaluate M w f) ↔ ∀ a ∈ P α ℓ, evaluate M w (⌈⌈a⌉⌉ψ))