(symbol-fix x) is a fixing function for symbolp; it is the
identity for symbols and coerces non-symbols to
Unfortunately it's not currently possible to come up with a good symbol-fixing function that induces the proper congruences for both symbol-name and symbol-package-name. This definition at least gives us a congruence for symbol-name.
BOZO consider adding a symbolp guard, inlining it, and turning it into an identity function for execution.
(defun symbol-fix (x) (declare (xargs :guard t)) (if (symbolp x) x '||))
(defthm symbolp-of-symbol-fix (symbolp (symbol-fix x)) :rule-classes :type-prescription)
(defthm symbol-fix-when-symbolp (implies (symbolp x) (equal (symbol-fix x) x)))