simp
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : ℕ → ℕ → σ
g : ℕ × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (n m : ℕ), g (n, m) (List.map (fun i => f i.unpair.1 i.unpair.2) (List.range (n.pair m))) = some (f n m)
this✝¹ : Primrec₂ fun p => g p.2
this✝ : Primrec₂ fun x i => f i.1 i.2
this : Primrec₂ fun n m => (fun x i => f i.1 i.2) () (n, m)
⊢ ∀ (a b : ℕ), (fun x i => f i.1 i.2) () (a, b) = f a b
no goals