theorem Hex.GraphIso.Nauty.Sparse.Fill.mem_iff {before : Array Nat} {data : List Nat} {first : Nat} {after : Array Nat} {n q : Nat} (h : Fill before data first data.length after) (hp : after.toList.Perm (List.range n)) (hq : q < n) : after[q]! ∈ data ↔ first ≤ q ∧ q < first + data.length

In a valid labelling, a copied vertex occurs in the copied interval and nowhere else.

theorem Hex.GraphIso.Nauty.Sparse.Fill.scatter {before : Array Nat} {data : List Nat} {first : Nat} {after : Array Nat} {n : Nat} {starts out : Array Nat} {value : Nat} (h : Fill before data first data.length after) (hp : after.toList.Perm (List.range n)) (hw : Index.Writes n starts out data value) : Index.Scatter n after starts out first (first + data.length) value

The vertex writes of reverse reinsertion are exactly a scatter along the completed label interval.