exact ⟨Semiformula.lMap (Language.oringEmb : ℒₒᵣ →ᵥ L) p, Hierarchy.oringEmb Hp,
  by 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
⊢ ∃ p_1, Hierarchy Γ ν p_1 ∧ (Semiformula.lMap Language.oringEmb) (∀ᶠ* succInd p) = ∀ᶠ* succInd p_1
no goals