The command has indeed failed with message:
No product even after head-reduction.
The command has indeed failed with message:
Not an inductive product.
The command has indeed failed with message:
Not an inductive product.