∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {xs : List α} {xc : (x : α) × Fin (List.count x xs)},
  0 < (List.filter (fun x => x == (xs.idxToSigmaCount (xs.sigmaCountToIdx xc)).fst) xs).length