theorem Hex.GraphIso.Nauty.Sparse.specLeaves_map {n : Nat} (G H : SparseGraph n) (p : Perm n) (hiso : ∀ (u v : Fin n), H.adj (p.get u) (p.get v) = G.adj u v) (tcLevel fuel level : Nat) (lab out ptn : Array Nat) (active : VSet n) (numcells : Nat) (hg : SpecNode G level lab ptn active numcells) (hh : SpecNode H level out ptn active numcells) (hcell : cellsPerm ptn level out (Array.map (renamingOf p).toFun lab)) {leaf : SpecLeaf n} (hm : leaf ∈ specLeaves G tcLevel fuel level lab ptn active numcells) : SpecLeaf.map p leaf ∈ specLeaves H tcLevel fuel level out ptn active numcells

Every leaf of the executed unpruned sparse tree transports under an isomorphism and arbitrary orders within corresponding input cells. The induction includes every target member and preserves the entire code chain.