case func f v ih => funext i; exact ih i
L : Language
μ : Type v
n arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → Semiterm L μ n
ih : ∀ (a : Fin arity✝), (↑(ofSubterm (v a))).toSubterm ⋯ = v a
⊢ (fun i => (↑(ofSubterm (v i))).toSubterm ⋯) = v
no goals