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

State before:
L : Language
hz : Operator.Zero L
ho : Operator.One L
ha : Operator.Add L
z : ℕ
⊢ z + 1 ≠ 0
Tactic:
simp
State after:
no goals