Theorem: LO.FirstOrder.UTerm.subtEquiv_func (Logic/FirstOrder/Computability/Term.lean)

State before:
L : Language
μ : Type v
n k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
⊢ (func f fun i => ↑(subtEquiv (v i))).bv ≤ n
Tactic:
simp[bv]
State after:
no goals