Theorem: LO.FirstOrder.Arith.Hierarchy.bit (Arithmetization/ISigmaOne/Bit.lean)

State before:
ξ : Type u_1
n : ℕ
μ : Type u_2
Γ : Polarity
s : ℕ
t u : Semiterm ℒₒᵣ μ n
⊢ Hierarchy Γ s (“!!t ∈ !!u”)
Tactic:
simp[Semiformula.Operator.operator, Matrix.fun_eq_vec₂, operator_mem_def]
State after:
no goals