Remove equidq.
Remove equidq.

The proof is not an intuitionistic one, the theorem is not used
anywhere, and it isn't really clear it is especially needed for
investigating the intuitionistic axioms.

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