Performance note. In the execution, this is just an inlined call of eql.
Function:
(defun maybe-pos-equiv$inline (x y) (declare (xargs :guard (and (maybe-posp x) (maybe-posp y)))) (eql (maybe-posp-fix x) (maybe-posp-fix y)))
Theorem:
(defthm maybe-pos-equiv-is-an-equivalence (and (booleanp (maybe-pos-equiv x y)) (maybe-pos-equiv x x) (implies (maybe-pos-equiv x y) (maybe-pos-equiv y x)) (implies (and (maybe-pos-equiv x y) (maybe-pos-equiv y z)) (maybe-pos-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm maybe-pos-equiv-implies-equal-maybe-posp-fix-1 (implies (maybe-pos-equiv x x-equiv) (equal (maybe-posp-fix x) (maybe-posp-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm maybe-posp-fix-under-maybe-pos-equiv (maybe-pos-equiv (maybe-posp-fix x) x) :rule-classes (:rewrite :rewrite-quoted-constant))