  The most dramatic result obtained by a type-theory-plus-ambiguity-axiom analysis came when Ronald Jensen [1969] noticed that if we weaken TST to a theory called TSTU by allowing the existence of urelemente (distinct empty sets) then it is easy to prove the consistency of the axioms of typical ambiguity. The result is a model of NFU, which is NF with extensionality weakened to allow urelemente. Jensen referred to NFU as “slight(?) modification of Quine’s NF”, but – as he showed – the modification has huge effects: Specker’s proof of the axiom of infinity no longer works, and AC is not refutable either.