simp only [filter, filterSpec]
case cons
α✝ : Type u_1
p : α✝ → Bool
x : α✝
xs : List α✝
ih : filter p xs = filterSpec p xs
⊢ filter p (x :: xs) = filterSpec p (x :: xs)
case cons
α✝ : Type u_1
p : α✝ → Bool
x : α✝
xs : List α✝
ih : filter p xs = filterSpec p xs
⊢ (match p x with
    | true => x :: filter p xs
    | false => filter p xs) =
    if p x = true then x :: filterSpec p xs else filterSpec p xs