cases em (evaluate M w τ)
W : Type
M : KripkeModel W
w : W
τ : Formula
L : List Formula
α : Program
L_def : τ :: L = testsOfProgram α
IH :
  ∀ (α : Program),
    L = testsOfProgram α →
      ∃ a, a.Sublist (testsOfProgram α) ∧ ∀ a_1 ∈ testsOfProgram α, evaluate M w (if a_1 ∈ a then a_1 else ~a_1)
⊢ ∃ a, a.Sublist (τ :: L) ∧ ∀ a_1 ∈ τ :: L, evaluate M w (if a_1 ∈ a then a_1 else ~a_1)
case inl
W : Type
M : KripkeModel W
w : W
τ : Formula
L : List Formula
α : Program
L_def : τ :: L = testsOfProgram α
IH :
  ∀ (α : Program),
    L = testsOfProgram α →
      ∃ a, a.Sublist (testsOfProgram α) ∧ ∀ a_1 ∈ testsOfProgram α, evaluate M w (if a_1 ∈ a then a_1 else ~a_1)
h✝ : evaluate M w τ
⊢ ∃ a, a.Sublist (τ :: L) ∧ ∀ a_1 ∈ τ :: L, evaluate M w (if a_1 ∈ a then a_1 else ~a_1)

case inr
W : Type
M : KripkeModel W
w : W
τ : Formula
L : List Formula
α : Program
L_def : τ :: L = testsOfProgram α
IH :
  ∀ (α : Program),
    L = testsOfProgram α →
      ∃ a, a.Sublist (testsOfProgram α) ∧ ∀ a_1 ∈ testsOfProgram α, evaluate M w (if a_1 ∈ a then a_1 else ~a_1)
h✝ : ¬evaluate M w τ
⊢ ∃ a, a.Sublist (τ :: L) ∧ ∀ a_1 ∈ τ :: L, evaluate M w (if a_1 ∈ a then a_1 else ~a_1)