simp[depth_eq_elimDecode]
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
this : Primrec₂ (elimDecode β fun a l => l.sup + 1)
⊢ ∀ (a b : ℕ), elimDecode β (fun a l => l.sup + 1) a b = Option.map (fun w => (↑w).depth) (decode b)
no goals