The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Fri, May 4, 2012 at 9:36 PM, Randy Pollack 
<rpollack0 AT gmail.com>
 wrote:
> Hurken's paradox, TLCA 1995.

Umm, could you be more specific?  When I tried a Google search on
those terms, all I got was some random Agda patch where "Hurken's
paradox" was just by itself in the middle with no context.  And afaict
HurkensParadox.v in the Coq source would require something like
Axiom classicT : forall {X:Type}, X + (X -> False).
-- 
Daniel Schepler