cases' x with x <;> simp
case hb
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.ex.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x < p.bv
⊢ (if x = 0 then UTerm.bvar x else UTerm.bShifts 1 (b₁ (x - 1))) =
    if x = 0 then UTerm.bvar x else UTerm.bShifts 1 (b₂ (x - 1))
case hb.succ
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.ex.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x + 1 < p.bv
⊢ UTerm.bShifts 1 (b₁ x) = UTerm.bShifts 1 (b₂ x)