induction t <;> simp[ofSubterm, toSubterm]
L : Language
μ : Type v
n : ℕ
t : UTerm L μ
h : t.bv ≤ n
⊢ ↑(ofSubterm (t.toSubterm h)) = t
case func
L : Language
μ : Type v
n arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → UTerm L μ
a_ih✝ : ∀ (a : Fin arity✝) (h : (a✝ a).bv ≤ n), ↑(ofSubterm ((a✝ a).toSubterm h)) = a✝ a
h : (func a✝¹ a✝).bv ≤ n
⊢ (fun i => ↑(ofSubterm ((a✝ i).toSubterm ⋯))) = a✝