∀ {α : Type u_1} {x : α} [inst : BEq α] (head : α) (tail : List α),
  1 ≤ (List.filter (fun x_1 => x_1 == x) (head :: tail)).length →
    0 < (List.findIdxs (fun x_1 => x_1 == x) (head :: tail)).length