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