intro W M w
L : List Formula
α : Program
L_def : L = testsOfProgram α
⊢ tautology (dis (List.map (signature α) (allTP α)))
L : List Formula
α : Program
L_def : L = testsOfProgram α
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (dis (List.map (signature α) (allTP α)))