Theorem: LO.FirstOrder.Semiterm.Operator.numeral_zero (Logic/FirstOrder/Basic/Operator.lean)

State before:
L : Language
hz : Operator.Zero L
ho : Operator.One L
ha : Operator.Add L
⊢ numeral L 0 = op(0)
Tactic:
rfl
State after:
no goals