simp only [filterSpec, h₂, ite_true]
case cons.true
α : Type u_1
p₁ p₂ : α → Bool
x : α
xs : List α
ih : filterSpec p₁ (filterSpec p₂ xs) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
h₂ : p₂ x = true
⊢ filterSpec p₁ (filterSpec p₂ (x :: xs)) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) (x :: xs)
case cons.true
α : Type u_1
p₁ p₂ : α → Bool
x : α
xs : List α
ih : filterSpec p₁ (filterSpec p₂ xs) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
h₂ : p₂ x = true
⊢ (if p₁ x = true then x :: filterSpec p₁ (filterSpec p₂ xs) else filterSpec p₁ (filterSpec p₂ xs)) =
    if decide (True ∧ p₁ x = true) = true then x :: filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
    else filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs