case h
α : Type u_1
β : Type ?u.371824
γ : Type ?u.371827
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : α → Fin n → σ
h : Primrec₂ f
a : α
i : Fin n
⊢ Vector.get (Vector.ofFn fun i => f a i) i = f a i
α : Type u_1
β : Type ?u.371824
γ : Type ?u.371827
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : α → Fin n → σ
h : Primrec₂ f
a : α
⊢ Vector.get (Vector.ofFn fun i => f a i) = f a
funext i
no goals
case h
α : Type u_1
β : Type ?u.371824
γ : Type ?u.371827
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : α → Fin n → σ
h : Primrec₂ f
a : α
i : Fin n
⊢ Vector.get (Vector.ofFn fun i => f a i) i = f a i
simp