rcases Nat.lt_or_eq_of_le h with (lt | rfl)
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s s' : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
h : s ≤ s'
⊢ Hierarchy Γ s' p
case inl
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s s' : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
h : s ≤ s'
lt : s < s'
⊢ Hierarchy Γ s' p

case inr
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
h : s ≤ s
⊢ Hierarchy Γ s p