Intuitionize riotaex in iset.mm
Intuitionize riotaex in iset.mm

Rename to reuiotaex and add an existential uniqueness condition
(similar to iset.mm euiotaex replacing set.mm iotaex ).

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