Int-equiv
Equivalence under ifix, i.e., integer equivalence.
Definitions and Theorems
Theorem: int-equiv-implies-equal-zip-1
(defthm int-equiv-implies-equal-zip-1
(implies (int-equiv a a-equiv)
(equal (zip a) (zip a-equiv)))
:rule-classes (:congruence))
