Note that you can expand iota-based definitions with riotacl2 or iotacl
Note that you can expand iota-based definitions with riotacl2 or iotacl

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 ...".

Here we document a general strategy to do this, using riotacl2 (or iotacl
for unbounded iota), as demonstrated in the proof of supub.

This captures information from an email by Mario Carneiro on
Thu, 13 Jul 2017 10:12:31 +0100.  We want to capture hints like this
in the set.mm database itself, both to help people creating new proofs
and also to help people understand the existing proofs.

Signed-off-by: David A. Wheeler <9ae72d22d8b894b865a7a496af4fab6320e6abb2@dwheeler.com>

metamath/set.mm,metamath/set.mm,metamath/set.mm