have hm : Primrec (fun p => p.2 : α × ℕ → ℕ) := snd
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
t : α → ℕ → α
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
ht : Primrec₂ t
hg : Primrec₂ g
H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)
⊢ Primrec₂ f
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
t : α → ℕ → α
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
ht : Primrec₂ t
hg : Primrec₂ g
H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)
hm : Primrec fun p => p.2
⊢ Primrec₂ f