English
Let a be an element of α and f a function Fin n → α. For any i in Fin(n+1), the value obtained by placing a in front of f and evaluating at i.rev matches the value obtained by appending a at the end of the reversed tail (f ∘ rev) evaluated at i.
Русский
Пусть a ∈ α и f: Fin n → α. Для любого i ∈ Fin(n+1) значение, полученное при конструировании cons a f и взятии на позиции i.rev, равно значению snoc (f ∘ rev) a в позиции i.
LaTeX
$$$$\mathrm{cons}\ (\alpha := \mathsf{fun}\ _\to\ \alpha)\ a\ f\ i.rev = \mathrm{snoc}\ (\alpha := \mathsf{fun}\ _\to\ \alpha)\ (f \circ \mathrm{Fin.rev})\ a\ i$$$$
Lean4
theorem cons_rev {α n} (a : α) (f : Fin n → α) (i : Fin <| n + 1) :
cons (α := fun _ => α) a f i.rev = snoc (α := fun _ => α) (f ∘ Fin.rev : Fin _ → α) a i := by
simpa using insertNth_rev 0 a f i
