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

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