have := elim_primrec (L := L) (μ := μ) 0 0 (const 0) (const 0) (succ.comp₂ nat_max) (succ.comp₂ nat_max) succ succ
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec depth
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this :
  Primrec
    (elim 0 0 (fun {k} f v => 0) (fun {k} f v => 0) (fun a b => (max a b).succ) (fun a b => (max a b).succ) Nat.succ
      Nat.succ)
⊢ Primrec depth