Rules for init-value-to-value.
Theorem: init-value-to-value-when-single
(defthm init-value-to-value-when-single (implies (and (valuep val) (equal (type-of-value val) type)) (equal (init-value-to-value type (init-value-single val)) val)))