no goals
α✝ : Type ?u.68744
β✝ : Type ?u.68747
σ✝ : Type ?u.68750
inst✝⁵ : Primcodable α✝
inst✝⁴ : Primcodable β✝
inst✝³ : Primcodable σ✝
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Denumerable α
inst✝¹ : Denumerable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ (Primrec fun n => f (ofNat (α × β) n).fst (ofNat (α × β) n).snd) ↔
    Primrec (Nat.unpaired fun m n => f (ofNat α m) (ofNat β n))
simp