no goals
α : Type u_3
β : Type u_1
σ : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
g : α → β
hf : Primrec f
hg : Primrec g
n : ℕ
⊢ (Nat.casesOn (encode (decode n)) 0 fun n =>
      encode (Option.map f (decode (Nat.pred (encode (Option.map g (decode n))))))) =
    encode (Option.map (fun a => f (g a)) (decode n))
cases @decode α _ n <;> simp [encodek]