theorem Hex.GraphIso.Nauty.refine_discrete_iff {n k : Nat} {G : Colored n k} {ctx : Ctx n} (hn0 : 0 < n) {level numcells : Nat} {st : Search n} (hok : SearchOk G level numcells st) (hlevel : 1 ≤ level) : (refine ctx level st.lab st.ptn st.active numcells).numcells = n ↔ discreteAt (refine ctx level st.lab st.ptn st.active numcells).ptn level n = true

Under the search invariant, the search's refined cell-count guard agrees with the specification's discreteness guard.

theorem Hex.GraphIso.Nauty.SubtreeOk.ofFrames {n : Nat} {ctx : Ctx n} {level : Nat} {r r' : RefineSt n} (h : SubtreeOk ctx level r) (hlab : r'.lab = r.lab) (hptn : r'.ptn = r.ptn) (hcells : r'.numcells = r.numcells) : SubtreeOk ctx level r'

The subtree facts ignore the refinement bookkeeping fields.