rw [← L_def]
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))
W : Type
M : KripkeModel W
w : W
α : Program
L_def : [] = testsOfProgram α
⊢ ∃ a, a.Sublist [] ∧ evaluate M w (Con (List.map (fun τ => if ↑τ ∈ a then ↑τ else ~↑τ) [].attach))