> -- (or define a cartesian product type instead of using the library's sigma > types) It seems that _x_ should not be defined the way it is in the standard library.