Let's let $\def\OP#1#2{\left\langle#1,#2\right\rangle}\OP xy$ represent the set $\{\{x\},\{x,y\}\}$ as is usual, per Kuratowski. Then:
$ \begin{eqnarray} \OP{\OP ab}c & = & \{\{\{\{a\}, \{a,b\}\}\}, \{\{\{a\}, \{a, b\}\}, c\}\} \\ \OP x{\OP yz} & = & \{\{x\}, \{x, \{\{y\}, \{y,z\}\}\}\} \end{eqnarray} $
I would like to unify these two equations to produce a set of relations on $a,b,c,x,y,z$ that give the most general conditions for which $ \OP{\OP ab}c = \OP x{\OP yz}$.
The unification algorithm I know works on expressions. Applying it to $ \OP{\OP ab}c = \OP x{\OP yz}$ directly gives $x=\OP ab, c=\OP yz$. This is correct, but may not be the most general possible set of conditions.
I can also abbreviate $\{x\}$ as $Sx$ and $\{y,z\}$ as $Dyz$, so that $\OP xy = \{\{x\}, \{x, y\}\} = DSxDxy$. Then the two set expressions I want to unify become $DSDSaDabDDSaDabc$ and $DSxDxDSyDyz$. I can unify these; the result is the same as in the previous paragraph.
But this may not be fully general, because it fails to capture the fact that for sets, $\{a, a\} = \{a\}$. Abbreviating $\{x\}$ as $Sx$ and $\{y,z\}$ as $Dyz$, and attempting to unify $\{x\}$ and $\{y, z\}$ with this method fails outright. But I want it to succeed and to yield the equations $x=y, x=z$.
How can I fix either the unification algorithm or my representation of the expressions to allow $\{x\}$ to unify with $\{y, z\}$?
I can make some progress on this particular problem by representing $\{x\}$ as $Dxx$. Then $\{x\}$ unifies with $\{y,z\}$ because $Dxx$ unifies with $Dyz$ giving $x=y, x=z$ as I wanted.
But this is not quite enough either, because it doesn't understand that $\{x, y\} = \{y, x\}$. I want the unification of $\{x, y\}$ with $\{a, b\}$ to give me not simply $x=a, y=b$ but $[x=a, y=b] \lor [x=b, y=a]$.
The problem grows worse if any of the sets have more than two elements. There are several possible ways in which $\{x, y\}$ could unify with $\{a,b,c\}$. For example, we might have $x=a=c, y=b$, or $x=c, y=a=b$.
Is there a modified version of the unification algorithm that can handle unification of sets in this way?