rw [filter_eq_filterSpec, filter_eq_filterSpec, filter_eq_filterSpec]
α : Type u_1
p₁ p₂ : α → Bool
xs : List α
⊢ filter p₁ (filter p₂ xs) = filter (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs
α : Type u_1
p₁ p₂ : α → Bool
xs : List α
⊢ filterSpec p₁ (filterSpec p₂ xs) = filterSpec (fun x => decide (p₂ x = true ∧ p₁ x = true)) xs