intro x hx
case hb
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
t : Semiterm L μ k
⊢ ∀ x < (↑(subtEquiv t)).bv, (if x < k then UTerm.bvar (x + 1) else default) = UTerm.bvar (x + 1)
case hb
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
t : Semiterm L μ k
x : ℕ
hx : x < (↑(subtEquiv t)).bv
⊢ (if x < k then UTerm.bvar (x + 1) else default) = UTerm.bvar (x + 1)