rcases Nat.eq_or_lt_of_le (Nat.zero_le s) with (rfl | pos)
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
b b' : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy b 0 p
⊢ Hierarchy b' s p
case inl
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
b b' : Polarity
p : Semiformula L μ n
hp : Hierarchy b 0 p
⊢ Hierarchy b' 0 p

case inr
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
b b' : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy b 0 p
pos : 0 < s
⊢ Hierarchy b' s p