by_cases hm₂ : x < m₂
case h
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ 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₁)))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
case pos
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : x < m₂
⊢ (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₁)))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))

case neg
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
⊢ (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₁)))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))