no goals
α : Type u_1
β : Type ?u.370940
γ : Type ?u.370943
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : Fin n → α → σ
h : ∀ (i : Fin n), Primrec (f i)
a : Fin n × α
⊢ Vector.get (Vector.ofFn fun i => f i a.snd) a.fst = f a.fst a.snd
simp