∀ {α : Type u_1} [inst_1 : DecidableEq α] (w : α),
  List.idxOfNth w [] 0 + 1 ≤ (List.filter (fun x => decide (x = w)) []).length →
    List.idxOfNth w [] 0 < (List.filter (fun x => decide (x = w)) []).length