induction m <;> simp[Matrix.conj, Matrix.vecTail, *]
L : Language
inst✝ : L.LT
μ : Type v
m n : ℕ
Γ : Polarity
s : ℕ
p : Fin m → Semiformula L μ n
⊢ Hierarchy Γ s (Matrix.conj p) ↔ ∀ (i : Fin m), Hierarchy Γ s (p i)
case succ
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
⊢ (Hierarchy Γ s (p 0) ∧ ∀ (i : Fin n✝), Hierarchy Γ s (p i.succ)) ↔ ∀ (i : Fin (n✝ + 1)), Hierarchy Γ s (p i)