Note 16
This type constructor, a purely specification-time phenomenon, has no corresponding syntax.