have : Primrec₂ (elimDecode β (fun a l => l.sup + 1)) :=
  primrec_elimDecode β (by simp only [← Nat.succ_eq_add_one]; apply Primrec.succ.comp $ (list_sup nat_max).comp snd)
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
⊢ Primrec₂ fun s e => Option.map (fun w => (↑w).depth) (decode e)
α : 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)
⊢ Primrec₂ fun s e => Option.map (fun w => (↑w).depth) (decode e)