no goals
α : Type u_1
β : Type ?u.18969
σ : Type ?u.18972
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
n : ℕ
⊢ encode (decode n) = encode (Option.map encode (decode n))
cases @decode α _ n <;> rfl