intro h
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
⊢ Hierarchy Γ s p → Hierarchy Γ s ((Semiformula.lMap Language.oringEmb) p)
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula ℒₒᵣ μ n
h : Hierarchy Γ s p
⊢ Hierarchy Γ s ((Semiformula.lMap Language.oringEmb) p)