Represents a tagged union member name.
This is a product type introduced by defprod.
We use a custom representation for the names of tagged union member names so that we do not confuse them with ordinary vl-id-p objects.