∀ {ι : Type u_1} [inst : BEq ι] [inst_1 : LawfulBEq ι] (a : ι) (l : List ι) (n : ℕ) (hi : n + 1 < (a :: l).length)
  (w : ι) (h_5 : (a == (a :: l)[n + 1]) = true) (h_8 : (((a :: l).erase (a :: l)[n + 1])[n] == w) = true),
  (List.findIdxs (fun x => x == w) (a :: l))[0] < (a :: l).length