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

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