Intuitionize elxp4 in iset.mm
Intuitionize elxp4 in iset.mm

Although the change from the set.mm proof is not really more than
"change snex to snexg", this is an involved change which carries
A e. _V through much of the proof and only at the end shows that
both sides of the equivalence imply A e. _V . The statement of
elxp4 does not need to change.

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