Theorem: LO.FirstOrder.UTerm.bind_bind (Logic/FirstOrder/Computability/Term.lean)

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
μ₃ : Type u_3
t : UTerm L μ₁
b₁ : ℕ → UTerm L μ₂
e₁ : μ₁ → UTerm L μ₂
b₂ : ℕ → UTerm L μ₃
e₂ : μ₂ → UTerm L μ₃
⊢ bind b₂ e₂ (bind b₁ e₁ t) = bind (fun x => bind b₂ e₂ (b₁ x)) (fun x => bind b₂ e₂ (e₁ x)) t
Tactic:
induction t <;> simp[bind, *]
State after:
no goals