ext x <;> simp [Rew.comp_app]
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
⊢ Rew.toS.comp (Rew.rewriteMap (Semiformula.fvListing σ)) =
    (Rew.castLE ⋯).comp (Rew.toS.comp (Rew.rewriteMap ((Semiformula.lMap Φ) σ).fvListing))
case hb
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
x : Fin 0
⊢ Rew.toS #x = (Rew.castLE ⋯) (Rew.toS #x)

case hf
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
x : ξ
⊢ Semiformula.fvListing σ x = Fin.castLE ⋯ (((Semiformula.lMap Φ) σ).fvListing x)