rcases decode n <;> simp[WType.encode_eq, WType.SubWType.ofW]
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
this : Primrec fun n => Option.map (fun e => e.unpair.1) (encodeDecode (WType β) n)
n : ℕ
⊢ Option.map ((fun e => e.unpair.1) ∘ encode) (decode n) = Option.map depth (decode n)
no goals