English
If f is Primrec' and g is a vector-valued Primrec', then the function v ↦ List.Vector.cons (f v) (g v) is Primrec'.
Русский
Если f примитивно-рекурсивна, а g — векторно-примитивно-рекурсивна, то v ↦ конc (f v) (g v) примитивно-рекурсивна.
LaTeX
$$$$ \\forall n \\forall m \\forall f:\\mathrm{List.Vector}\\ \\mathbb{N}\\ n \\to \\mathbb{N}, \\forall g:\\mathrm{List.Vector}\\ \\mathbb{N}\\ n \\to \\mathrm{List.Vector}\\ \\mathbb{N}\\ m,\\ \\mathrm{Primrec'}\\ f \\to \\mathrm{Vec}\\ g \\to \\operatorname{Primrec'}\\big( \\lambda v, \\mathrm{List.Vector}.cons (f\,v) (g\,v) \\big). $$$$
Lean4
protected theorem cons {n m f g} (hf : @Primrec' n f) (hg : @Vec n m g) : Vec fun v => f v ::ᵥ g v := fun i =>
Fin.cases (by simp [*]) (fun i => by simp [hg i]) i
