theorem Hex.GraphIso.Nauty.Sparse.Limited.sweepStep_eq {n : Nat} {descend : Generic.NodeFn (State n)} {plainDescend : Generic.NodeFn (Sparse.State n)} {next : Generic.SweepFn (State n) n} {plainNext : Generic.SweepFn (Sparse.State n) n} (hd : NodeEq descend plainDescend) (hn : SweepEq next plainNext) (inf : Nat) (first : Bool) (level nc tc tv1 tv index : Nat) (cell : VSet n) (s : State n) (h : Ready (Generic.sweepStep inf descend next first level nc tc tv1 tv cell index s).snd.snd) : Ready s ∧ sweepValue (Generic.sweepStep inf descend next first level nc tc tv1 tv cell index s) = Generic.sweepStep inf plainDescend plainNext first level nc tc tv1 tv cell index s.value

One bounded sibling step projects to the native step, including first-child cleanup, orbit skips and nonlocal child returns.