theorem Hex.GraphIso.Nauty.Sparse.Graph.context_map {n : Nat} (G H : SparseGraph n) (p : Perm n) (h : ∀ (u v : Fin n), H.adj (p.get u) (p.get v) = G.adj u v) : RowsMap (renamingOf p) (context G).g (context H).g

A native graph isomorphism transports the proof interpretation of its rows. This changes no graph representation in the executable.

theorem Hex.GraphIso.Nauty.Sparse.perm_map {n : Nat} {lab : Array Nat} (hp : lab.toList.Perm (List.range n)) (p : Perm n) : (Array.map (renamingOf p).toFun lab).toList.Perm (List.range n)

Applying the vertex permutation to every raw label entry preserves the label-permutation contract.