simp [Formula.lMap_fvUnivClosure, succInd, Semiformula.lMap_substs]
L : Language
inst✝¹ : L.ORing
ξ : Type u_1
inst✝ : DecidableEq ξ
Γ : Polarity
ν : ℕ
p : Semiformula ℒₒᵣ ℕ 1
Hp : Hierarchy Γ ν p
⊢ (Semiformula.lMap Language.oringEmb) (∀ᶠ* succInd p) = ∀ᶠ* succInd ((Semiformula.lMap Language.oringEmb) p)
no goals