∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (a : α) (l : List α),
  (l.Nodup → ∀ (i : ℕ) (h : i < l.length), l.erase l[i] = l.eraseIdx i) →
    (a :: l).Nodup → ∀ (i : ℕ) (h : i + 1 < (a :: l).length), (a :: l).erase (a :: l)[i + 1] = (a :: l).eraseIdx (i + 1)