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

State before:
L✝ : Language
inst✝² : L✝.LT
μ : Type v
L : Language
inst✝¹ : L.Eq
inst✝ : L.LT
n : ℕ
Γ : Polarity
s : ℕ
t u : Semiterm L μ n
⊢ Hierarchy Γ s (“!!t = !!u”)
Tactic:
simp[Semiformula.Operator.operator, Matrix.fun_eq_vec₂,
  Semiformula.Operator.Eq.sentence_eq]
State after:
no goals