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

State before:
ξ : Type u_1
n : ?m.44108
⊢ op(∈).sentence = HSemiformula.val bitDef
Tactic:
simp [Semiformula.Operator.Mem.mem, Semiformula.Operator.operator]
State after:
no goals