Rules about type-of-value.
These rules rewrite type-of-value to specific types under hypotheses on different types of values that occur during symbolic execution.
Theorem:
(defthm type-of-value-when-value-pointer (implies (and (valuep x) (value-case x :pointer)) (equal (type-of-value x) (type-pointer (value-pointer->reftype x)))))
Theorem:
(defthm type-of-value-of-if* (equal (type-of-value (if* a b c)) (if* a (type-of-value b) (type-of-value c))))