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

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q : Semiformula L μ n
⊢ Hierarchy Γ s (p ⟶ q) ↔ Hierarchy Γ.alt s p ∧ Hierarchy Γ s q
Tactic:
simp[Semiformula.imp_eq]
State after:
no goals