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