theorem Hex.GraphIso.Nauty.Sparse.Sort.indirect_congr {y z : Array Nat} {start len : Nat} {x : Array Nat} (h : Agree y z start (start + len) x) : indirect x y start len = indirect x z start len

The full executed indirect sort returns literally equal arrays when the key arrays agree on the requested segment. The proof follows the actual bounded stack, including its exact push and tie order.