rw [disEval]
L : List Formula
α : Program
L_def : L = testsOfProgram α
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (dis (List.map (signature α) (allTP α)))
L : List Formula
α : Program
L_def : L = testsOfProgram α
W : Type
M : KripkeModel W
w : W
⊢ ∃ f ∈ List.map (signature α) (allTP α), evaluate M w f