cases i using Fin.cases <;> simp[*]
case intro
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
a✝ : ∀ {p : Fin n✝ → Semiformula L μ n}, Hierarchy Γ s (Matrix.conj p) ↔ ∀ (i : Fin n✝), Hierarchy Γ s (p i)
p : Fin (n✝ + 1) → Semiformula L μ n
hz : Hierarchy Γ s (p 0)
hs : ∀ (i : Fin n✝), Hierarchy Γ s (p i.succ)
i : Fin (n✝ + 1)
⊢ Hierarchy Γ s (p i)
no goals