no goals
α : Type u_2
β✝ : Type ?u.27049
σ : Type ?u.27052
inst✝² : Primcodable α
inst✝¹ : Primcodable β✝
inst✝ : Primcodable σ
β : Type u_1
e : β ≃ α
this : Primcodable β := Primcodable.ofEquiv α e
⊢ Primrec fun a => encode (↑e (↑e.symm a))
simp [Primrec.encode]