Fixtype of the ATJ types that denote built-in ACL2 types.
This is a tagged union type, introduced by fty::deftagsum.
See atj-type.