funext i
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (rel r v).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ (fun i => UTerm.bind b₁ (fun x => e₂ x) (v i)) = fun i => UTerm.bind b₂ (fun x => e₂ x) (v i)
case h
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (rel r v).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
i : Fin k
⊢ UTerm.bind b₁ (fun x => e₂ x) (v i) = UTerm.bind b₂ (fun x => e₂ x) (v i)