simp [TP,signature,allTP]
W : Type
M : KripkeModel W
w : W
α : Program
L_def : [] = testsOfProgram α
⊢ ∃ f ∈ List.map (signature α) (allTP α), evaluate M w f
W : Type
M : KripkeModel W
w : W
α : Program
L_def : [] = testsOfProgram α
⊢ ∃ a,
    a.Sublist (testsOfProgram α) ∧
      evaluate M w (Con (List.map (fun τ => if ↑τ ∈ a then ↑τ else ~↑τ) (testsOfProgram α).attach))