theorem Hex.GraphIso.Nauty.Generation.process_short {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hclear : st.needshortprune = false) (hshort : (processnode ctx level numcells st).snd.needshortprune = true) : (processnode ctx level numcells st).fst ≠ Int.ofNat st.gcaFirst

A fresh short-prune request never returns to the current first-path guide. The guiding child can subsequently change that guide; an off-path child cannot.