Totality checker improvements (soundness)

When spotting a cycle, need to check that the decreasing argument
is in the same position.

For the moment, this means we can't spot decreasing arguments which
change position across multiple calls - but soundness is more
important!