simp[List.ofFnNthVal]
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
n : ℕ
v : σ → Fin n → α
f : σ → Fin n
hv : Primrec v
hf : Primrec f
this : Primrec fun x => (List.ofFn (v x)).get? ↑(f x)
x : σ
⊢ (List.ofFn (v x)).get? ↑(f x) = some (v x (f x))
no goals