induction xs with
| nil => simp [filterSpec]
| cons x xs ih =>
  cases h₂ : p₂ x with
  | false =>
    simp only [filterSpec, h₂, ite_false]
    exact ih
  | true =>
    simp only [filterSpec, h₂, ite_true]
    cases h₁ : p₁ x with
    | false =>
      simp only [filterSpec, h₁, h₂, ite_false]
      exact ih
    | true =>
      simp only [filterSpec, h₁, h₂, ite_true]
      exact congrArg _ ih
α : Type u_1
p₁ p₂ : α → Bool
xs : List α
⊢ filterSpec p₁ (filterSpec p₂ xs) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
no goals