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