Note that List may contain non-ground terms. If Sorted
is unbound at call-time, for each consequtive pair of elements in
Sorted, the relation
E1 @< E2 will hold.
However, unifying a variable in Sorted may cause this
relation to become invalid,
even unifying a variable in Sorted with another
(older) variable. See also section