simp [Formula.fvUnivClosure, Semiformula.lMap_toS, Semiformula.lMap_rewriteMap]
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
⊢ (Semiformula.lMap Φ) (∀ᶠ* σ) = ∀ᶠ* (Semiformula.lMap Φ) σ
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 Φ) σ))