Definition succ_eq
Definition.
succ_eq
succ n = n ∪ {n}
The successor operation for ordinal numbers, in particular for
onat
.