Add nnmsuc to iset.mm
Add nnmsuc to iset.mm

Includes adding onmsuc and removing an unused distinct variable
constraint from the onasuc theorem. Here we follow the lead of
nnasuc which is simplified from the set.mm approach.

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