apply ih
case cons.e_tail
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ removeAllEq xs [x] = xs

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x
case cons.e_tail
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ ¬x ∈ xs

case cons.a
α : Type u_1
inst✝ : DecidableEq α
x x' : α
xs : List α
ih : ¬x ∈ xs → removeAllEq xs [x] = xs
hnmem : ¬x ∈ x' :: xs
⊢ x' ≠ x