some more properties about STRING_SORT
WIP: more reworking of treatment of term valuations

make them apply to a list of the values of the (sorted) type variables,
to make the dependence completely explicit...