simpa using H
α : 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
⊢ ∀ (a : Unit) (n m : ℕ),
    g (a, n, m).2 (List.map (fun i => (fun x i => f i.1 i.2) a i.unpair) (List.range (n.pair m))) =
      some ((fun x i => f i.1 i.2) a (n, m))
no goals