Completely revise sptree toSortedAList impl

The original implementation of toSortedAList was overcomplicated, using
auxiliary run-length-encoding functions to carry across the idea of the
algorithm from one that works on a dense structure.

After a couple of rounds of adjustment and simplification, the proof is quite a
bit simpler, and the new version does have aux constants but they should all
translate into cv or CakeML AST without any additional fiddling.