Modify proof of dveeq2 to be intuitionistic.
Modify proof of dveeq2 to be intuitionistic.

Turns out that distinctors can function in intuitionistic logic, at
least given ax-i12 and the intuitionistic propositional logic
such as orel2.

Reduces "show usage ax-3/recursive" count by 10.

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