no goals
α : Type u_1
β : Type ?u.368006
γ : Type ?u.368009
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : Fin n → α → σ
hf : ∀ (i : Fin n), Primrec (f i)
⊢ Primrec fun a => Vector.toList (Vector.ofFn fun i => f i a)
simp [list_ofFn hf]