no goals
α : Type u_1
β : Type ?u.25349
σ : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → σ
h : Primrec fun a => encode (f a)
n : ℕ
⊢ encode (Option.map (fun a => encode (f a)) (decode n)) = encode (Option.map f (decode n))
cases @decode α _ n <;> rfl