Formally proving properties of fold function

Question

Recall the fold function for lists:

$fold(f,z,[x,xs]) = fold(f,f(z,x),xs)$

$fold(f,z,[]) = z$

I want to formally proof that if $f$ is associative, commutative and idempotent (meaning $f(x,y) = f(x,f(x,y))$ and we have to lists $l_1$ and $l_2$ such that their contents are equal then $fold(f,z,l_1) = fold(f,z,l_2)$.

What I've tried

1. I've tried double induction on the sizes of the list but this doesn't clarify much the problem.

2. I've figured out a procedure that would leave me with a list of non-repeating elements. I take each element of the $f(f(f(\cdots)))$ list and take it to the outside thanks to associative and commutative property. En each step I make sure that if I find two equal elements I remove them using idempotence. The basic rules are as follows:

$f(f(z,x),y) \text{ push x out, push y in} = f(y,f(z,x)) = f((y,z),x) = f(f(z,y),x)$

$f(f(z,x),x) = f(z,x)$

The actual transformation to the list would look like this:

     def transform[A](l: List[A]) := l match {
        case Nil() => Nil()
        case x :: Nil() => x :: Nil()
        case x :: x :: xs => transform(x :: xs)
        case x :: y :: xs  => y :: transform(x :: xs)  
     }

My first problem is how to write the predicate to say that this algorithm gives a list with non-repeating elements. I do it like this:

$\forall x,y. x \in l \land y \in l \land x = y \implies index(x) = index(y)$

But I don't how to proof that my algorithm guarantees that this property holds.

3. The idea is that if I can proof that this transformation does not leave repeating elements then it would be easy to show that the lists end up with equal lengths and for each first element of one list I could transform the second list to get the very first element and I could apply induction to show that the statement holds.

So in short, if you think my approach is efficient and correct do you know how to solve the problems I got? And if you think you have better ideas can you give me any hints?

Edit

Just realized that my function only eliminates one repeating sequence. So adapt the argument...