ALTERNATIVE ::= ... | SUBSORTS SUBSORTS ::= subsorts SORT+
A subsorts alternative is written:
sorts S1, ..., SnAs with sort declarations, the plural keyword may be written in the singular (regardless of the number of sorts).
The sorts Si, which must be already declared in the local environment, are declared to be embedded as subsorts of the sort declared by the enclosing datatype declaration. (`sorts S1, ..., Sn' and `sort S1 | ... | sort Sn' are equivalent.)
In a free datatype declaration, all the sorts that are embedded in the declared sort by the alternatives must have no common subsorts. When the alternatives of a free datatype declaration are all subsorts, the declared sort corresponds to the union of the subsorts.