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

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