intros x xs
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (x : α) (xs : List α), removeAllEq (x :: xs) [x] = removeAllEq xs [x]
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
⊢ removeAllEq (x :: xs) [x] = removeAllEq xs [x]