simp [hu]
case inr.inl
L : Language
μ : Type v
n : ℕ
t u : UTerm L μ
ht : t.bv ≤ n + 1
hu : u.bv ≤ n
hx : t.bv.pred < t.bv
⊢ (if t.bv.pred < t.bv.pred then bvar t.bv.pred else if t.bv.pred = t.bv.pred then u else bvar t.bv.pred.pred).bv ≤ n
no goals