induction h generalizing n₁ <;> try simp [Rew.eq_ball_iff, Rew.eq_bex_iff, Rew.eq_all_iff, Rew.eq_ex_iff] at hq ⊢
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ n₂
q : Semiformula L μ₂ n₂
hq : ω.hom p = q
h : StrictHierarchy Γ s q
⊢ StrictHierarchy Γ s p
case zero
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
x✝ s✝ : ℕ
Γ✝ : Polarity
p✝ : Semiformula L μ₂ x✝
a✝ : DeltaZero p✝
n₁ : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ x✝
hq : ω.hom p = p✝
⊢ StrictHierarchy Γ✝ s✝ p

case sigma
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
a✝ : StrictHierarchy 𝚷 s✝ p✝
a_ih✝ : ∀ {n₁ : ℕ} {p : Semiformula L μ₁ n₁} (ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)), ω.hom p = p✝ → StrictHierarchy 𝚷 s✝ p
n₁ : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ n✝
hq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∃' p'
⊢ StrictHierarchy 𝚺 (s✝ + 1) p

case pi
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
a✝ : StrictHierarchy 𝚺 s✝ p✝
a_ih✝ : ∀ {n₁ : ℕ} {p : Semiformula L μ₁ n₁} (ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)), ω.hom p = p✝ → StrictHierarchy 𝚺 s✝ p
n₁ : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ n✝
hq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∀' p'
⊢ StrictHierarchy 𝚷 (s✝ + 1) p

case ex
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
a✝ : StrictHierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : ∀ {n₁ : ℕ} {p : Semiformula L μ₁ n₁} (ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)), ω.hom p = p✝ → StrictHierarchy 𝚺 (s✝ + 1) p
n₁ : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ n✝
hq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∃' p'
⊢ StrictHierarchy 𝚺 (s✝ + 1) p

case all
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
a✝ : StrictHierarchy 𝚷 (s✝ + 1) p✝
a_ih✝ : ∀ {n₁ : ℕ} {p : Semiformula L μ₁ n₁} (ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)), ω.hom p = p✝ → StrictHierarchy 𝚷 (s✝ + 1) p
n₁ : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ n✝
hq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∀' p'
⊢ StrictHierarchy 𝚷 (s✝ + 1) p