English
The tail (vector without the first element) is primitive recursive.
Русский
Хвост вектора — хвостовой вектор без первого элемента — примитивно-рекурсивен.
LaTeX
$$$$ \\operatorname{Primrec}\\big( \\mathrm{List.Vector.tail} : \\mathrm{List.Vector}\\ \\alpha\\ n \\to \\mathrm{List.Vector}\\ \\alpha\\ (n-1) \\big). $$$$
Lean4
theorem vector_tail {n} : Primrec (@List.Vector.tail α n) :=
vector_toList_iff.1 <| (list_tail.comp vector_toList).of_eq fun ⟨l, h⟩ => by cases l <;> rfl