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