theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Ready.children {n : Nat} {G : SparseGraph n} {level : Nat} {s : RefineSt n} (h : Ready G level s) (hshape : NodeShape n level s.ptn) {tc len a b : Nat} (hc : IsCell s.ptn level tc len) (hb : tc + len ≤ n) (hn : 1 < len) (ha : a < len) (hb' : b < len) (scratch other : Scratch) (hs : Scratch.Bounded n scratch) (ht : Scratch.Bounded n other) : ∃ (p : Perm n), (∀ (i j : Fin n), G.adj (p.get i) (p.get j) = G.adj i j) ∧ Equiv (renamingOf p) (level + 1) (RefineSt.child (Graph.ofGraph G) level s tc s.lab[tc + a]! scratch) (RefineSt.child (Graph.ofGraph G) level s tc s.lab[tc + b]! other)

Any two actual cached children of the same cell below a cheap-shaped node correspond under a graph automorphism, including equal choices with different incoming scratch.