unfold F at *
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
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 ∈
        match α, ℓ with
        | ·a, x => ∅
        | ?'τ, ℓ => if ℓ ⟨τ, ⋯⟩ = true then ∅ else [~τ]
        | α⋓β, l => (F α fun τ => l ⟨↑τ, ⋯⟩) ∪ F β fun τ => l ⟨↑τ, ⋯⟩
        | α;'β, l => (F α fun τ => l ⟨↑τ, ⋯⟩) ∪ F β fun τ => l ⟨↑τ, ⋯⟩
        | ∗α, l =>
          F α fun x =>
            match x with
            | ⟨f, f_in⟩ => l ⟨f, ⋯⟩,
      evaluate M w f