theorem Hex.GraphIso.Nauty.Sparse.CountSort.finish_lab {n : Nat} (level first last : Nat) (distance : Bool) (s : RefineSt n) (w1 v2 w2 v3 : Nat) : (finish level first last distance s w1 v2 w2 v3).lab = if last = v2 then s.lab else if last = v3 then s.lab else «Sort».indirect s.lab s.hits v3 (last - v3)

Finalizing count fragments only changes labels at the one indirect sort call. The index, queue and hash updates retain that exact array.