intro τ τ_in
case refine_1
α : Program
ℓ : TP α
⊢ ∀ (τ : { τ // τ ∈ testsOfProgram α }), (~↑τ) ∈ F α ℓ → ℓ τ = false
case refine_1
α : Program
ℓ : TP α
τ : { τ // τ ∈ testsOfProgram α }
τ_in : (~↑τ) ∈ F α ℓ
⊢ ℓ τ = false