SUBSORT-DECL ::= subsort-decl SORT+ SORT
A subsort declaration SUBSORT-DECL is written:
s1, ..., sn < s
It declares all the sorts s1, ..., sn, and s, as well as the embedding of each si as a subsort of s. The si must be distinct from s.
When a subsort declaration occurs in a sort generation construct, the embedding and projection operations between the subsort(s) and the supersort are treated as declared operations with regard to generation of sorts.
Introducing an embedding relation between two sorts may cause operation symbols to become related by the overloading relation, so that values of terms become equated when the terms are identical up to embedding.