simp only [lt, ↓reduceIte, bv_bvar, ge_iff_le]
case inl
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x < t.bv.pred
this : x < n
⊢ (if x < t.bv.pred then bvar x else if x = t.bv.pred then u else bvar x.pred).bv ≤ n
case inl
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
x : ℕ
hx : x < t.bv
lt : x < t.bv.pred
this : x < n
⊢ x + 1 ≤ n