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