induction t <;> simp[elim, bv, *]
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)
t : UTerm L μ
⊢ elim Nat.succ (fun x => 0) (fun {k} x v => (List.ofFn v).sup) t = t.bv
case func
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)
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → UTerm L μ
a_ih✝ : ∀ (a : Fin arity✝), elim Nat.succ (fun x => 0) (fun {k} x v => (List.ofFn v).sup) (a✝ a) = (a✝ a).bv
⊢ (List.ofFn fun i => (a✝ i).bv).sup = Finset.univ.sup fun i => (a✝ i).bv