refine ⟨?_, ?_, ?_⟩
α : Program
ℓ : TP α
⊢ (∀ (τ : { τ // τ ∈ testsOfProgram α }), (~↑τ) ∈ F α ℓ → ℓ τ = false) ∧
    Con (F α ℓ)⋀signature α ℓ≡signature α ℓ ∧
      ∀ (ψ : Formula), Con (Xset α ℓ ψ)⋀signature α ℓ≡Con (List.map (fun αs => ⌈⌈αs⌉⌉ψ) (P α ℓ))⋀signature α ℓ
case refine_1
α : Program
ℓ : TP α
⊢ ∀ (τ : { τ // τ ∈ testsOfProgram α }), (~↑τ) ∈ F α ℓ → ℓ τ = false

case refine_2
α : Program
ℓ : TP α
⊢ Con (F α ℓ)⋀signature α ℓ≡signature α ℓ

case refine_3
α : Program
ℓ : TP α
⊢ ∀ (ψ : Formula), Con (Xset α ℓ ψ)⋀signature α ℓ≡Con (List.map (fun αs => ⌈⌈αs⌉⌉ψ) (P α ℓ))⋀signature α ℓ