theorem Hex.GraphIso.Nauty.Sparse.splitCounts_perm {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) (hf : first ≤ s.cellend[first]!) (hb : s.cellend[first]! < s.lab.size) : (splitCounts level first distance s).lab.toList.Perm s.lab.toList

The actual count splitter permutes the label array. The initial cell window is nonempty and bounded; no assumptions on the hit values are needed.