induction h <;> try simp[*]
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
h : Hierarchy Γ s p
⊢ Hierarchy Γ.alt s (~p)
case ball
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
a_ih✝ : Hierarchy Γ✝.alt s✝ (~p✝)
⊢ Hierarchy Γ✝.alt s✝ (“(∃[#0 < !!t✝] !(~p✝))”)

case bex
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
a_ih✝ : Hierarchy Γ✝.alt s✝ (~p✝)
⊢ Hierarchy Γ✝.alt s✝ (“(∀[#0 < !!t✝] !(~p✝))”)

case ex
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : Hierarchy 𝚺.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚷 (s✝ + 1) (∀' ~p✝)

case all
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
a_ih✝ : Hierarchy 𝚷.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚺 (s✝ + 1) (∃' ~p✝)

case sigma
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚷 s✝ p✝
a_ih✝ : Hierarchy 𝚷.alt s✝ (~p✝)
⊢ Hierarchy 𝚷 (s✝ + 1) (∀' ~p✝)

case pi
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 s✝ p✝
a_ih✝ : Hierarchy 𝚺.alt s✝ (~p✝)
⊢ Hierarchy 𝚺 (s✝ + 1) (∃' ~p✝)

case dummy_sigma
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚷 (s✝ + 1) p✝
a_ih✝ : Hierarchy 𝚷.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) (∃' ~p✝)

case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : Hierarchy 𝚺.alt (s✝ + 1) (~p✝)
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) (∀' ~p✝)