[zozbot234]

It is a formalization of Cantor's diagonal argument - in fact, of "diagonal arguments" more generally. See http://arxiv.org/abs/math/0305282 for an expository treatment.

[cubefox]

Thanks, looks interesting.