rw[Rew.eq_bind Rew.bShift, subtEquiv_bind_eq_bind]
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
⊢ ↑(subtEquiv (Rew.bShift t)) = bShifts 1 ↑(subtEquiv t)
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
⊢ UTerm.bind (fun x => if hx : x < k then ↑(subtEquiv ((⇑Rew.bShift ∘ bvar) ⟨x, hx⟩)) else default)
      (fun x => ↑(subtEquiv ((⇑Rew.bShift ∘ fvar) x))) ↑(subtEquiv t) =
    bShifts 1 ↑(subtEquiv t)