exact this.of_eq (fun t => by
  induction t <;> simp[elim, bv, *]
  { simp[List.sup_ofFn] })
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this : Primrec (elim Nat.succ (fun x => 0) fun {k} x v => (List.ofFn v).sup)
⊢ Primrec bv
no goals