simp [←Rew.hom_comp_app]
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
⊢ ∀* Rew.toS.hom ((Rew.rewriteMap (Semiformula.fvListing σ)).hom ((Semiformula.lMap Φ) σ)) =
    ∀* Rew.toS.hom ((Rew.rewriteMap ((Semiformula.lMap Φ) σ).fvListing).hom ((Semiformula.lMap Φ) σ))
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
⊢ ∀* (Rew.toS.comp (Rew.rewriteMap (Semiformula.fvListing σ))).hom ((Semiformula.lMap Φ) σ) =
    ∀* (Rew.toS.comp (Rew.rewriteMap ((Semiformula.lMap Φ) σ).fvListing)).hom ((Semiformula.lMap Φ) σ)