case nil =>
  simp [TP,signature,allTP]
  rw [← L_def]
  simp
W : Type
M : KripkeModel W
w : W
α : Program
L_def : [] = testsOfProgram α
⊢ ∃ f ∈ List.map (signature α) (allTP α), evaluate M w f
no goals