Description: Define Russell's definition description binder, which can be read as
"the unique x such that ph ", where ph ordinarily contains
x as a free variable. Our definition is meaningful only when there
is exactly one x such that ph is true (see iotaval );
otherwise, it evaluates to the empty set (see iotanul ). Russell used
the inverted iota symbol iota to represent the binder.

Sometimes proofs need to expand an iota-based definition. That is,
given "X = the x for which ... x ... x ..." holds, the proof needs to
get to "... X ... X ...". A general strategy to do this is to use
riotacl2 (or iotacl for unbounded iota), as demonstrated in the
proof of supub . This can be easier than applying riotasbc or a
version that applies an explicit substitution, because substituting an
iota into its own property always has a bound variable clash which must
be first renamed or else guarded with NF.