α : Type u_2
β : Type u_1
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ (Primrec fun p => f p.fst p.snd) ↔ Primrec₂ f
α : Type u_2
β : Type u_1
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ Primrec (Function.uncurry f) ↔ Primrec₂ f
rw [show Function.uncurry f = fun p : α × β => f p.1 p.2 from funext fun ⟨a, b⟩ => rfl]
no goals
α : Type u_2
β : Type u_1
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ (Primrec fun p => f p.fst p.snd) ↔ Primrec₂ f
rfl