rintro _ p Hp rfl
L : Language
inst✝¹ : L.ORing
ξ : Type u_1
inst✝ : DecidableEq ξ
Γ : Polarity
ν : ℕ
⊢ ∀ (a : Sentence ℒₒᵣ) (x : Semiformula ℒₒᵣ ℕ 1),
    Hierarchy Γ ν x → a = ∀ᶠ* succInd x → ∃ p, Hierarchy Γ ν p ∧ (Semiformula.lMap Language.oringEmb) a = ∀ᶠ* succInd p
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