have hq : Primrec (fun n => n.pred : ℕ → ℕ) := Primrec.pred
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 μ
hr : Primrec fun p => (List.map UTerm.bv (List.ofFn p.snd.2)).sup
hb : Primrec₂ fun m n => max m n
⊢ Primrec bv
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 μ
hr : Primrec fun p => (List.map UTerm.bv (List.ofFn p.snd.2)).sup
hb : Primrec₂ fun m n => max m n
hq : Primrec fun n => n.pred
⊢ Primrec bv