Intuitionize nfreu in iset.mm
Intuitionize nfreu in iset.mm

Replace nfreud with nfreudxy which has an additional distinct
variable constraint, on x and y. Likewise for nfreu to nfreuxy.

Some set.mm usages are already OK with that constraint, for the others
maybe we'll figure out how to remove it or maybe those proofs
will be changed some other way.

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