English
For any n and any f : α → List.Vector β n, the Primrec property of a → (f a).toList is equivalent to Primrec f.
Русский
Пусть n задано, и f : α → List.Vector β n. Примитивно-рекурсивность функции a ↦ (f(a).toList) эквивалентна примитивно-рекурсивности самой функции f.
LaTeX
$$$$ ( \\operatorname{Primrec}( \\lambda a, (f\\,a).toList ) ) \\iff ( \\operatorname{Primrec} f ). $$$$
Lean4
theorem vector_toList_iff {n} {f : α → List.Vector β n} : (Primrec fun a => (f a).toList) ↔ Primrec f :=
subtype_val_iff