Solution (source code)

= Solution

\b[This encoding works], interpreting the outer three-coordinate brackets by the nested <ordered pair> convention established in item 1. <Equality> of the outer <ordered triples> gives
$$
\{0,a\}=\{0,a'\},\qquad \{1,b\}=\{1,b'\},\qquad \{2,c\}=\{2,c'\}.
$$
For any fixed <set> $k$, the map $x\mapsto\{k,x\}$ is <injective>. If $x=k$, <equality> $\{k,x\}=\{k,y\}$ makes the right-hand side a <singleton> and forces $y=k$. If $x\ne k$, membership of $x$ in $\{k,y\}$ forces $x=y$. Applying this argument with $k=0,1,2$ recovers the respective coordinates.

The outer brackets must encode an <ordered triple>, rather than an unordered <set> of three doubletons. The source uses three-coordinate angle brackets here; using the successful convention of item 1 makes their meaning explicit and supplies a genuine construction.