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

State before:
L : Language
μ : Type v
z : ℕ
u : UTerm L μ
x : Fin z
⊢ substAt z u (bvar ↑x) = bvar ↑x
Tactic:
simp[substLast, substAt, bind]
State after:
no goals