simp[Semiformula.iff_eq]
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
b : Polarity
p q : Semiformula L μ n
⊢ Hierarchy b 0 (p ⟷ q) ↔ Hierarchy b 0 p ∧ Hierarchy b 0 q
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
n : ℕ
b : Polarity
p q : Semiformula L μ n
⊢ Hierarchy b 0 p → Hierarchy b 0 q → Hierarchy b 0 q ∧ Hierarchy b 0 p