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