 As Sol Feferman has pointed out, one place where the treatments in NFU (at least those given so far) are clearly quite involved are situations in which one needs to work with indexed families of objects. The proof of König’s Lemma of set theory in Holmes 1998 is a good example of how complicated this kind of thing can get in NFU. We have a notion that the use of sets of “Quine atoms” (self-singletons) as index sets (necessarily for s.c. sets) might relieve this difficulty, but we haven’t proved this in practice, and problems would remain for the noncantorian situation.