simp
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l✝ : List α
b : α
l : List α
m : ∀ (a' : α), a' ∈ l → b ≠ a'
a✝ : Pairwise (fun x x_1 => x ≠ x_1) l
IH : l.erase b = filter (fun x => x != b) l
⊢ ¬(b != b) = true
no goals