Same as prod-cons, but avoids reconsing like cons-with-hint.
We leave this enabled and expect to reason about prod-cons instead.
Function:
(defun prod-cons-with-hint$inline (x y hint) (declare (xargs :guard t)) (mbe :logic (prod-cons x y) :exec (and (or x y) (cons-with-hint x y hint))))