Modelling Set Intersection
Set Intersection and Set Difference can be modelled in the world of sequences by means of functions inter and subtract.
Both have the property that if ? and r do not contain any duplicate elements then neither does inter(?, r) nor substract(?, r).
Prove: ret(inter(?, r)) = ret ? ? ret r