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.