no goals
α : Type u_1
β : Type ?u.50685
γ : Type ?u.50688
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
⊢ Part.none = Part.bind ↑(decode n) fun a => map encode ((fun x => Part.none) a)
cases decode (α := α) n <;> simp