∀ {α : Type u_1} {x : α} [inst : BEq α] (head : α) (tail : List α) {n s : ℕ}
  {h : n < (List.idxsOf x (head :: tail) s).length},
  (head == x) = true → (List.idxsOf x (head :: tail) s)[0] - s < (head :: tail).length