include "Coq.ma".
-(*#***************************************************************************)
+include "Init/Prelude.ma".
-(* The Calculus of Inductive Constructions *)
+(*#***********************************************************************)
-(* *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* Projet LogiCal *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* *)
+(* \VV/ **************************************************************)
-(* INRIA LRI-CNRS *)
+(* // * This file is distributed under the terms of the *)
-(* Rocquencourt Orsay *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(* *)
+(*#***********************************************************************)
-(* May 29th 2002 *)
+(* Hurkens.v *)
-(* *)
-
-(*#***************************************************************************)
-
-(* Hurkens.v *)
-
-(*#***************************************************************************)
+(*#***********************************************************************)
(*#* This is Hurkens paradox [Hurkens] in system U-, adapted by Herman
Geuvers [Geuvers] to show the inconsistency in the pure calculus of