have hr : Primrec (fun p => ((List.ofFn p.2.2).map UTerm.bv).sup : (k : ℕ) × L.Rel k × (Fin k → UTerm L μ) → ℕ) :=
  (list_sup nat_max).comp
    (list_map (by apply sigma_finArrow_list_ofFn.comp (sigma_prod_right (β := L.Rel))) (UTerm.bv_primrec.comp₂ Primrec₂.right))
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 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
⊢ Primrec bv