(maybe-lit-fix x) is the identity for maybe-litps, or
coerces any non-litp to
Performance note. In the execution this is just an inlined identity function, i.e., it should have zero runtime cost.
(defun maybe-lit-fix$inline (x) (declare (xargs :guard (maybe-litp x))) (mbe :logic (if x (lit-fix x) nil) :exec x))
(defthm maybe-litp-of-maybe-lit-fix (maybe-litp (maybe-lit-fix x)) :rule-classes (:rewrite :type-prescription))
(defthm maybe-lit-fix-when-maybe-litp (implies (maybe-litp x) (equal (maybe-lit-fix x) x)))
(defthm maybe-lit-fix-under-iff (iff (maybe-lit-fix x) x))
(defthm maybe-lit-fix-under-lit-equiv (lit-equiv (maybe-lit-fix x) x))