theorem Hex.GraphIso.Nauty.Sparse.Index.exists_valid {n level : Nat} {lab ptn : Array Nat} (hp : lab.toList.Perm (List.range n)) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) : ∃ (s : Scratch), Valid n lab ptn level s.cellstart s.cellend

Every valid labelled partition admits a cell index, supplied by the proved executed indexer. Used to discharge index premises of fresh selectors.