include "Coq.ma".
-(*#***************************************************************************)
+(*#***********************************************************************)
-(* The Calculus of Inductive Constructions *)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* Projet LogiCal *)
+(* \VV/ **************************************************************)
-(* *)
+(* // * This file is distributed under the terms of the *)
-(* INRIA LRI-CNRS *)
+(* * GNU Lesser General Public License Version 2.1 *)
-(* Rocquencourt Orsay *)
-
-(* *)
-
-(* May 29th 2002 *)
-
-(* *)
-
-(*#***************************************************************************)
+(*#***********************************************************************)
(*#* This is a proof in the pure Calculus of Construction that
classical logic in Prop + dependent elimination of disjunction entails