O-finp
Recognizes if an ordinal is finite
We introduce the function o-finp which returns t for any
ordinal that is finite, else nil. This function is equivalent to the
function atom, and is introduced so that we can disable its
definition when dealing with ordinals (also see make-ord).
Function: o-finp
(defun o-finp (x)
(declare (xargs :guard t))
(atom x))
