intro W M w
case refine_3
α : Program
ℓ : TP α
ψ : Formula
⊢ Con (Xset α ℓ ψ)⋀signature α ℓ≡Con (List.map (fun αs => ⌈⌈αs⌉⌉ψ) (P α ℓ))⋀signature α ℓ
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 α ℓ)