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

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