Coerce a Boolean into a bitp.
Function: bool->bit$inline
(defun bool->bit$inline (x) (declare (xargs :guard t)) (if x 1 0))
Theorem: bitp-of-bool->bit
(defthm bitp-of-bool->bit (bitp (bool->bit x)))
