intro x
σ✝ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ✝
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
σ : Type u_5
inst✝¹ : Primcodable σ
inst✝ : UniformlyPrimcodable β
b : σ → (a : α) × β a
hb : Primrec b
this : Primrec fun x => (encode (b x)).unpair.2
⊢ ∀ (n : σ), (encode (b n)).unpair.2 = encode (b n).snd
σ✝ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁸ : Primcodable σ✝
inst✝⁷ : Primcodable α
inst✝⁶ : (a : α) → Fintype (β a)
inst✝⁵ : (a : α) → DecidableEq (β a)
inst✝⁴ : (a : α) → Primcodable (β a)
inst✝³ : PrimrecCard β
inst✝² : Primcodable γ
σ : Type u_5
inst✝¹ : Primcodable σ
inst✝ : UniformlyPrimcodable β
b : σ → (a : α) × β a
hb : Primrec b
this : Primrec fun x => (encode (b x)).unpair.2
x : σ
⊢ (encode (b x)).unpair.2 = encode (b x).snd