Formally proving properties of fold function
"contents are equal" implies that their lengths are equal, so you don't need double induction.  Instead, try single induction.  A straightforward induction argument on the length of the list should suffice.

I wouldn't suggest trying to remove repeated elements.  That is not necessary, and it is an unnecessary complication that turns a simple induction into something really complicated and messy (as you have discovered).