Theorem: LO.FirstOrder.Arith.Hierarchy.neg_iff (Logic/FirstOrder/Arith/Hierarchy.lean)

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
h : Hierarchy Γ s (~p)
⊢ Hierarchy Γ.alt s p
Tactic:
simpa using neg h
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
h : Hierarchy Γ.alt s p
⊢ Hierarchy Γ s (~p)
Tactic:
simpa using neg h
State after:
no goals