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.

    predicate IsInverted(xs: seq<int>, i: int, j: int) {
        0 <= i < j < |xs| && xs[i] > xs[j]
    }

    function inversionSet(xs: seq<int>): set<(int,int)> {
        set i,j | 0 <= i < j < |xs| && IsInverted(xs, i, j) :: (i,j)
    }

    function pairSetMap(ss: set<(int, int)>, i: int): set<(int, int)> 
    {
        set pair | pair in ss :: (pair.0 + i, pair.1 + i)
    }

    lemma {:verify } {:timelimit 30} {:vcs_split_on_every_assert} pairMapSize(xs: seq<int>, i: int)
        requires 0 <= i
        ensures |pairSetMap(inversionSet(xs), i)| == |inversionSet(xs)|
    {
        if inversionSet(xs) == {} {
            assert |inversionSet(xs)| == 0;
            assert pairSetMap(inversionSet(xs), i) == {};
            assert |pairSetMap(inversionSet(xs), i)| == 0;
        }else{
            // forall x | x in inversionSet(xs)
            //     ensures (x.0+i, x.1+i) in pairSetMap(inversionSet(xs), i)
            // {

            // }

            // forall x | x in pairSetMap(inversionSet(xs), i)
            //     ensures (x.0-i, x.1-i) in inversionSet(xs)
            // {

            // }
            var ixs := inversionSet(xs);
            var pxs := pairSetMap(inversionSet(xs), i);
            var x :| x in inversionSet(xs);
            assert (x.0+i, x.1+i) in pxs;
            assert |ixs| == 1 + |ixs-{x}|;
            assert |pxs| == 1 + |pxs-{(x.0+i, x.1+i)}|;
            var removed: set<(int, int)> := {};
            var premoved: set<(int, int)> := {};
            var mixs := 0;
            var mpxs := 0;
            while ixs != {} 
                invariant ixs == inversionSet(xs)-removed
                invariant ixs <= inversionSet(xs)
                invariant ixs !! removed
                invariant pxs == pairSetMap(inversionSet(xs), i)-premoved
                invariant pxs <= pairSetMap(inversionSet(xs), i)-premoved
                invariant pxs !! premoved
                invariant forall x :: x in removed ==> (x.0+i, x.1+i) in premoved
                invariant forall x :: x in premoved ==> (x.0-i, x.1-i) in removed
                invariant mixs == |removed|
                invariant mpxs == |premoved|
                invariant mixs == mpxs
            {
                var x :| x in ixs;
                assert x !in removed;
                var mx := (x.0+i, x.1+i);
                assert mx !in premoved by {
                    if mx in premoved {
                        assert x in removed;
                        assert false;
                    }
                }
                assert mx in pxs;
                ixs := ixs - {x};
                pxs := pxs - {mx};
                mixs := mixs + 1;
                mpxs := mpxs + 1;
                removed := removed + {x};
                premoved := premoved + {mx};
            }
            assert ixs == {};
            assert pxs == {};
            assert removed == inversionSet(xs);
            assert premoved == pairSetMap(inversionSet(xs), i);
            calc {
                |inversionSet(xs)|;
                |removed|;
                mixs;
                mpxs;
                |premoved|;
                |pairSetMap(inversionSet(xs), i)|;
            }

        }

This answer doesn't go into why above code is not able to verify but an alternate solution which I am able to verify. I discovered it in process of writing recursive definition of pairSetMap. If I removed first post condition and only keep size post condition then some thinking will reveal that post condition doesn't necessary holds if (s.0 + i, s.1 + i) is already in pairSetMap(ss - {i}). This nudged me to write first post condition. Now all it needs was some asserts in else part.

predicate IsInverted(xs: seq<int>, i: int, j: int) {
    0 <= i < j < |xs| && xs[i] > xs[j]
}

function inversionSet(xs: seq<int>): set<(int,int)> {
    set i,j | 0 <= i < j < |xs| && IsInverted(xs, i, j) :: (i,j)
}

method pairSetMap(ss: set<(int, int)>, i: int) returns (r: set<(int, int)>) 
  ensures forall p :: p in ss <==> (p.0 + i, p.1 + i) in r
  ensures |r| == |ss|
{
    if |ss| < 1 {
      r := set pair | pair in ss :: (pair.0 + i, pair.1 + i);
    }
    else { 
        var s :| s in ss;
        var t := pairSetMap(ss - {s}, i);
        assert |t| == |ss - {s}|;
        assert |ss| == |ss - {s}| + 1;
        assert (s.0 + i, s.1 + i) !in t by {
           if (s.0 + i, s.1 + i) in t {
                assert (s.0, s.1) in ss - {s};
                assert (s.0, s.1) !in ss - {s};
           }
        }
        r := t + { (s.0 + i, s.1 + i) };
        assert |r| == |t| + 1;
    }
}