Rules for simplifying away value-result-fix.
Theorem: value-result-fix-when-valuep
(defthm value-result-fix-when-valuep (implies (valuep x) (equal (value-result-fix x) x)))