simp
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.all.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x + 1 < p.bv
⊢ x < p.all.bv
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.all.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x + 1 < p.bv
⊢ x < p.bv - 1