How to induct on mapped sets or…?
Working on verifying a version of the counting inversions algorithm. I feel like pairMapSize has everything it needs but it times out instead. I could try to do induction on slices of the array but I would need to define a function to produce another set, like the set of all inversions starting at (xs[0], YY) but then it would be just another case of comparing sets sizes.