Apalache type annotations for Cat.tla, applied via INSTANCE so the original spec remains free of tool-specific idiosyncrasies.