Positional operations on function-indexed lists

Reversal, cyclic movement of the first entry, and positional deletion act on the original finite index type. Empty output words and repeated values are retained. These identities supply actual scope coordinates without a distinctness assumption on values.

theorem List.reverse_ofFn {α : Type u_1} {n : ℕ} (f : Fin n → α) : (ofFn f).reverse = ofFn fun (i : Fin n) => f i.rev

Reversing the finite word reverses its positional indices, even when values repeat.

theorem List.ofFn_cons_finRotate {α : Type u_1} {n : ℕ} (a : α) (f : Fin n → α) : ofFn (Fin.cons a f ∘ ⇑(finRotate (n + 1))) = ofFn f ++ [a]

Positive cyclic index rotation moves the first list entry to the end, retaining every position even when values repeat.

theorem List.eraseIdx_ofFn {α : Type u_1} {n : ℕ} (f : Fin (n + 1) → α) (j : Fin (n + 1)) : (ofFn f).eraseIdx ↑j = ofFn fun (i : Fin n) => f (j.succAbove i)

Deleting one actual list position retains the succAbove order of all survivors. This is positional deletion, not value deletion, and allows repeated values.