simp [conEval, signature, F]
case refine_2
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con (F α ℓ)⋀signature α ℓ) ↔ evaluate M w (signature α ℓ)
case refine_2
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
⊢ (∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f) →
    ∀ f ∈ F α ℓ, evaluate M w f