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