Remove theorems from iset.mm which need dtru
Remove theorems from iset.mm which need dtru

Some of these we might get back if/when we get dtru .

- nfnid and nfcvb are interesting enough, but are also
little used.

- dtruALT is also non-intuitionistic, as it relies on being
able to say whether y is empty (in which case we pick { (/) }
as a different set) or non-empty (in which case we pick (/)
as a different set), and we don't get to do that kind of
excluded middle type logic.

- dtrucor , dtrucor2 , dvdemo1 , and dvdemo2 are not used in
set.mm. They demonstrate various concepts and thus might be
worth bringing back in the future, but no particular reason
we need them now.

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