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

State before:
L : Language
μ : Type v
t : UTerm L μ
m₁ m₂ : ℕ
⊢ bShifts m₂ (bShifts m₁ t) = bShifts (m₁ + m₂) t
Tactic:
simp[bShifts, bind_bind, bind, add_assoc]
State after:
no goals