I'm having trouble proving this within a while loop in Dafny:

assert multiset(seqa) == multiset(seqa[..i] + seqa[i..]);

Note:

• An invariant exists ensuring that 0 <= i <= |seqa|.

• There are no modifications to seqa throughout the loop.

I was able to successfully assert that

assert multiset(seqa) == multiset(seqa[..0] + seqa[0..]);

as the base case for the induction proof, but am unsure how to proceed.

assert multiset(seqa) == multiset(seqa[..0+i] + seqa[0+i..]);

is obviously not passing, but it seemed intuitive to think of it in that way.

Any advice/help is appreciated!