Simprocs for type "nat" no longer introduce numerals unless they are already
present in the expression, and in a coefficient position (i.e. as a factor
of a monomial).
recdef sep "measure (%(a,xs). length xs)"
"sep(a, x#y#zs) = x # a # sep(a,y#zs)"
"sep(a, xs) = xs"