Fixtype of ATJ function type information.
This is a product type introduced by fty::defprod.
In general, each ACL2 function has, associated with it, a primary (`main') function type and zero or more secondary (`other') function types, as mentioned in atj-types.