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