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

State before:
L : Language
μ : Type v
z : ℕ
u : UTerm L μ
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ
⊢ substAt z u (func f v) = func f fun i => substAt z u (v i)
Tactic:
simp[substLast, substAt, bind]
State after:
no goals