simp
L : Language
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
m : ℕ
e : μ₁ → UTerm L μ₂
t : UTerm L μ₁
ht : t.bv ≤ m
he : ∀ (x : μ₁), (e x).bv ≤ m
x : ℕ
hx : x < t.bv
⊢ (bvar x).bv ≤ m
L : Language
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
m : ℕ
e : μ₁ → UTerm L μ₂
t : UTerm L μ₁
ht : t.bv ≤ m
he : ∀ (x : μ₁), (e x).bv ≤ m
x : ℕ
hx : x < t.bv
⊢ x + 1 ≤ m