apply UTerm.bShifts_primrec.comp
  (fst.comp $ snd.comp $ fst.comp $ fst.comp $ fst.comp fst)
  (he.comp (fst.comp $ fst.comp $ fst.comp $ fst.comp fst) snd)
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
hb : Primrec₂ b
he : Primrec₂ e
⊢ Primrec₂ fun x x_1 => UTerm.bShifts x.1.1.1.2.1 (e x.1.1.1.1 x_1)
no goals