simp[bind, bv]
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, (b x).bv ≤ m) → (bind b e (v a)).bv ≤ m
hb : ∀ x < (func f v).bv, (b x).bv ≤ m
⊢ (bind b e (func f v)).bv ≤ m
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, (b x).bv ≤ m) → (bind b e (v a)).bv ≤ m
hb : ∀ x < (func f v).bv, (b x).bv ≤ m
⊢ ∀ (b_1 : Fin k), (bind b e (v b_1)).bv ≤ m