∀ {α : Type u_1} [inst : BEq α] {x : α} (head : α) (tail : List α),
  List.idxOf x (head :: tail) < (head :: tail).length →
    ¬List.idxOf x (head :: tail) = 0 → List.idxOf x (head :: tail) - 1 < tail.length