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