exact False.elim (Nat.not_le_of_lt lt this)
case inr.inr
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 ≤ t.bv.pred
⊢ (if x < t.bv - 1 then bvar x else if x = t.bv - 1 then u else bvar (x - 1)).bv ≤ n
no goals