English
If f is Partrec' on n and g is Partrec' on n+1, then the function v ↦ (f v).map (λ a => g (a :: v)) is Partrec' n.
Русский
Если f — Partrec' на n, а g — Partrec' на n+1, то функция v ↦ (f v).map (λ a, g(a :: v)) есть Partrec' n.
LaTeX
$$$$\\forall \\{n\\} \\{f : \\mathrm{List.Vector} \\mathbb{N} n \\to \\mathbb{N}\\} \\{g : \\mathrm{List.Vector} \\mathbb{N} (n+1) \\to \\mathbb{N}\\},\\; \\mathrm{Partrec'}(f) \\to \\mathrm{Partrec'}(n+1)(g) \\to \\mathrm{Partrec'}(n)\\;\\bigl(\\lambda v. (f\,v).\\mathrm{map}(\\lambda a. g(a\\,::\\,v))\\bigr).$$$$
Lean4
theorem of_eq {n} {f g : List.Vector ℕ n →. ℕ} (hf : Partrec' f) (H : ∀ i, f i = g i) : Partrec' g :=
(funext H : f = g) ▸ hf
