unfold shiftb
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ : ℕ
⊢ shiftb (shiftb b m₁) m₂ = shiftb b (m₁ + m₂)
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ : ℕ
⊢ (fun x =>
      if x < m₂ then UTerm.bvar x
      else UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁)))) =
    fun x => if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))