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