theorem Hex.GraphIso.Nauty.Sparse.splitSingleton_lab {n : Nat} (G : SparseGraph n) (level split : Nat) (s t : RefineSt n) (hs : RefineSt.Valid level s) (ht : RefineSt.Valid level t) (hl : t.lab = s.lab) (he : t.ptn = s.ptn) (hb : split < n) : (splitSingleton (Graph.ofGraph G) level split s).lab = (splitSingleton (Graph.ofGraph G) level split t).lab

Reusing admissible scratch cannot change the literal label array of the executed singleton splitter. The retained marks and generations may differ; the observed predicate is fixed by the native graph row.