This is Hurkens paradox
Hurkens in system U-, adapted by Herman
Geuvers
Geuvers to show the inconsistency in the pure calculus of
constructions of a retract from Prop into a small type.
References:
- Hurkens A. J. Hurkens, "A simplification of Girard's paradox",
Proceedings of the 2nd international conference Typed Lambda-Calculi
and Applications (TLCA'95), 1995.
- Geuvers "Inconsistency of Classical Logic in Type Theory", 2001
(see http://www.cs.kun.nl/~herman/note.ps.gz).