theorem
Hex.GraphIso.Nauty.Sparse.distvals_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)
(root v : Fin n)
:
Native BFS distances commute with an arbitrary supplied isomorphism, including unreachable vertices and changes to native traversal order.