simp [Theory.indH, Theory.indScheme]
L : Language
inst✝¹ : L.ORing
ξ : Type u_1
inst✝ : DecidableEq ξ
Γ : Polarity
ν : ℕ
⊢ ⇑(Semiformula.lMap Language.oringEmb) '' indScheme ℒₒᵣ (Hierarchy Γ ν) ⊆ indScheme L (Hierarchy Γ ν)
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