intro α
L : List Formula
⊢ ∀ (α : Program), L = testsOfProgram α → tautology (dis (List.map (signature α) (allTP α)))
L : List Formula
α : Program
⊢ L = testsOfProgram α → tautology (dis (List.map (signature α) (allTP α)))