theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Ready.setLab {n : Nat} {G : SparseGraph n} {level : Nat} {s : RefineSt n} (h : Ready G level s) (lab : Array Nat) (hsize : lab.size = s.lab.size) (hcells : cellsPerm s.ptn level lab s.lab) : Ready G level { lab := lab, ptn := s.ptn, active := s.active, queue := s.queue, cellstart := s.cellstart, cellend := s.cellend, indexed := s.indexed, hits := s.hits, marks := s.marks, vmarks := s.vmarks, stamp := s.stamp, numcells := s.numcells, longcode := s.longcode }

Reordering labels within the cells of a frozen equitable node retains its node and refinement-certificate invariants. The partition and its saved active set remain those of the ancestor witness.