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

case cons
W : Type
M : KripkeModel W
w : W
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : ∀ (α : Program), tail✝ = testsOfProgram α → ∃ f ∈ List.map (signature α) (allTP α), evaluate M w f
α : Program
L_def : head✝ :: tail✝ = testsOfProgram α
⊢ ∃ f ∈ List.map (signature α) (allTP α), evaluate M w f