Same as cdr, but guarded with prod-consp.
We leave this enabled and expect to reason about car instead.
Function: prod-cdr$inline
(defun prod-cdr$inline (x) (declare (xargs :guard (prod-consp x))) (cdr x))
