Fixtype of identifiers.
This is a product type introduced by fty::defprod.
We use ACL2 strings, which suffice to represent identifiers, and in fact can represent also more than that. This is is not an issue for the abstract syntax (it is only an issue for the concrete syntax), and provides some potential flexibility, e.g. for transforming code.