unfold F at *
case refine_1
α : Program
ℓ : TP α
τ : { τ // τ ∈ testsOfProgram α }
τ_in : (~↑τ) ∈ F α ℓ
⊢ ℓ τ = false
case refine_1
α : Program
ℓ : TP α
τ : { τ // τ ∈ testsOfProgram α }
τ_in :
  (~↑τ) ∈
    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, ⋯⟩
⊢ ℓ τ = false