no goals
α : Type u_1
β : Type ?u.22417
σ : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
x : σ
n : ℕ
⊢ (Nat.casesOn (encode (decode n)) 0 fun x_1 => Nat.succ (encode x)) = encode (Option.map (fun x_1 => x) (decode n))
cases @decode α _ n <;> rfl