theorem Hex.GraphIso.Nauty.Sparse.DescPath.map {n : Nat} (G H : SparseGraph n) (p : Perm n) (hiso : ∀ (i j : Fin n), H.adj (p.get i) (p.get j) = G.adj i j) {base last : Nat} {root leaf other : RefineSt n} {path : List (Nat × Nat)} (hpath : DescPath G base root path last leaf) (hr : RefineSt.Ready G base root) (ht : RefineSt.Ready H base other) (he : RefineSt.Equiv (renamingOf p) base root other) : ∃ (out : RefineSt n), ∃ (path' : List (Nat × Nat)), DescPath H base other path' last out ∧ List.map Prod.fst path' = List.map Prod.fst path ∧ RefineSt.Equiv (renamingOf p) last leaf out

Transport an entire literal native descent under an isomorphism. Target positions, depths and refinement observations agree; corresponding vertices may occupy different offsets within a tied cell.