iset.mm: clean ups to ax-16 comments and usage
iset.mm: clean ups to ax-16 comments and usage

Bring over the comment from set.mm about "obsolete" and
"New usage is discouraged".

Remove text about logical redundancy; that has not (yet at least)
been proved for intuitionistic logic.

Change two proofs to use ax16 instead of ax-16, since we consider
the latter to be obsolete.

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