no goals
α : Type u_1
β : Type ?u.140489
γ : Type ?u.140492
δ : Type ?u.140495
σ : Type ?u.140498
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
⊢ Primrec₂ fun p a => encode a
exact encode_iff.mpr snd
no goals
α : Type u_1
β : Type ?u.140489
γ : Type ?u.140492
δ : Type ?u.140495
σ : Type ?u.140498
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
⊢ Primrec₂ fun p a => p.fst
exact fst.comp fst