theorem Hex.GraphIso.Nauty.Sparse.splitCounts_outside {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) (hf : first ≤ s.cellend[first]!) (hb : s.cellend[first]! < s.lab.size) (q : Nat) (hq : q < first ∨ s.cellend[first]! < q) : (splitCounts level first distance s).lab[q]! = s.lab[q]!

The actual count splitter changes labels only inside its original cell.