have : x < n := by simpa using lt_of_lt_of_le lt (Nat.pred_le_pred ht)
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
⊢ (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
⊢ (if x < t.bv.pred then bvar x else if x = t.bv.pred then u else bvar x.pred).bv ≤ n