Rules about type-of-value-option.
These rules reduce type-of-value-option
to type-of-value when the argument is a value,
and to
Theorem:
(defthm type-of-value-option-when-valuep (implies (valuep x) (equal (type-of-value-option x) (type-of-value x))))
Theorem:
(defthm type-of-value-option-of-nil (equal (type-of-value-option nil) (type-void)))