simp[Function.comp]
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
n n' : ℕ
this : Primrec₂ fun v t => (Rew.bind v fun x => &x) t
v : Fin n → Semiterm L μ n'
p : Semiterm L μ n
⊢ (Rew.bind v fun x => &x) p = (Rew.bind (⇑(Rew.substs v) ∘ bvar) (⇑(Rew.substs v) ∘ fvar)) p
no goals