rw [Rew.eq_bind Rew.toS, lMap_bind]
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
p : Semiformula L₁ (Fin n) 0
⊢ (lMap Φ) (Rew.toS.hom p) = Rew.toS.hom ((lMap Φ) p)
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
p : Semiformula L₁ (Fin n) 0
⊢ (Rew.bind (Semiterm.lMap Φ ∘ ⇑Rew.toS ∘ Semiterm.bvar) (Semiterm.lMap Φ ∘ ⇑Rew.toS ∘ Semiterm.fvar)).hom
      ((lMap Φ) p) =
    Rew.toS.hom ((lMap Φ) p)