Intuitionize indexed intersection of X in iset.mm
Intuitionize indexed intersection of X in iset.mm

This is iindif2 (renamed to iindif2m ), iinin2 (renamed to
iinin2m ), and iinin1 (renamed to iinin1m ).

In each case the statement of the theorem and proof
change nonempty to inhabited.

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