induction p generalizing b₁ b₂ e₁ e₂ <;> simp[bind, bindq, he]
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
p : UFormula L μ₁
hb : ∀ x < p.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ bind b₁ e₁ p = bind b₂ e₂ p
case rel
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
arity✝ : ℕ
a✝¹ : L.Rel arity✝
a✝ : Fin arity✝ → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (rel a✝¹ a✝).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ (fun i => UTerm.bind b₁ (fun x => e₂ x) (a✝ i)) = fun i => UTerm.bind b₂ (fun x => e₂ x) (a✝ i)

case nrel
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
arity✝ : ℕ
a✝¹ : L.Rel arity✝
a✝ : Fin arity✝ → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (nrel a✝¹ a✝).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ (fun i => UTerm.bind b₁ (fun x => e₂ x) (a✝ i)) = fun i => UTerm.bind b₂ (fun x => e₂ x) (a✝ i)

case and
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
a✝¹ a✝ : UFormula L μ₁
a_ih✝¹ :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < a✝¹.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ a✝¹ = bind b₂ e₂ a✝¹
a_ih✝ :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < a✝.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ a✝ = bind b₂ e₂ a✝
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (a✝¹.and a✝).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ bindq b₁ e₁ 0 a✝¹ = bindq b₂ e₂ 0 a✝¹ ∧ bindq b₁ e₁ 0 a✝ = bindq b₂ e₂ 0 a✝

case or
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
a✝¹ a✝ : UFormula L μ₁
a_ih✝¹ :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < a✝¹.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ a✝¹ = bind b₂ e₂ a✝¹
a_ih✝ :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < a✝.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ a✝ = bind b₂ e₂ a✝
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (a✝¹.or a✝).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ bindq b₁ e₁ 0 a✝¹ = bindq b₂ e₂ 0 a✝¹ ∧ bindq b₁ e₁ 0 a✝ = bindq b₂ e₂ 0 a✝

case all
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
a✝ : UFormula L μ₁
a_ih✝ :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < a✝.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ a✝ = bind b₂ e₂ a✝
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < a✝.all.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ bindq b₁ e₁ 1 a✝ = bindq b₂ e₂ 1 a✝

case ex
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
a✝ : UFormula L μ₁
a_ih✝ :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < a✝.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ a✝ = bind b₂ e₂ a✝
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < a✝.ex.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ bindq b₁ e₁ 1 a✝ = bindq b₂ e₂ 1 a✝