induction xs with
| nil => rfl
| cons x' xs ih =>
  rw [removeAllEq_singleton_hd_neq]
  congr
  apply ih
  intro hneg
  apply hnmem
  apply Mem.tail
  . exact hneg
  . intro hneg'
    rw [hneg'] at hnmem
    apply hnmem
    apply Mem.head
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x : α
hnmem : ¬x ∈ xs
⊢ removeAllEq xs [x] = xs
no goals