System U is an inconsistent PTS in that one has a term of type $\bot = \forall p\colon \ast \ldotp p$, and such a term is explicitly constructed in Hurkens' A Simplification of Girard's Paradox.

One-sorted circular PTS $\lambda\ast$ ($S = \{\ast \}, A=\{\ast\colon \ast\}, R=\{(\ast,\ast)\}$) (Geuvers' Logics and Type Systems, p.78) is also inconsistent since a term of type $\bot$ in System U can be translated into $\lambda\ast$ by mapping $\ast, \square$ and $\triangle$ to $\ast$.

Is there any easier way to construct a term of type $\bot$ in $\lambda\ast$? Smaller terms, or constructions easier to understand, are appreciated.