SORTED-TERM ::= sorted-term TERM SORT
A sorted term is written:
T:s
It is well-sorted for some sort if the component term T is well-sorted for the specified sort s. It then expands to those of the fully-qualified expansions of the component term that have the specified sort.