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

State before:
L : Language
μ : Type v
t : UTerm L μ
⊢ bShifts 0 t = t
Tactic:
simp[bShifts]
State after:
L : Language
μ : Type v
t : UTerm L μ
⊢ bind (fun x => bvar x) fvar t = t

State before:
L : Language
μ : Type v
t : UTerm L μ
⊢ bind (fun x => bvar x) fvar t = t
Tactic:
induction t <;> simp[bind, *]
State after:
no goals