case func f v ih =>
  funext i
  have h : ∀ i, (v i).bv ≤ n := by simpa[bv] using h
  exact ih i (h i)
L : Language
μ : Type v
n arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → UTerm L μ
ih : ∀ (a : Fin arity✝) (h : (v a).bv ≤ n), ↑(ofSubterm ((v a).toSubterm h)) = v a
h : (func f v).bv ≤ n
⊢ (fun i => ↑(ofSubterm ((v i).toSubterm ⋯))) = v
no goals