transcript: we now check for non-existing objects

[helm.git] / helm / software / matita / contribs / procedural / Coq / Logic / Diaconescu.mma

diff --git a/helm/software/matita/contribs/procedural/Coq/Logic/Diaconescu.mma b/helm/software/matita/contribs/procedural/Coq/Logic/Diaconescu.mma
index 1947fdb0e049af7c02dd0fa17fe3c82497a7fd35..bf411f8095303e58381227d6881972ed4729ad40 100644 (file)
--- a/helm/software/matita/contribs/procedural/Coq/Logic/Diaconescu.mma
+++ b/helm/software/matita/contribs/procedural/Coq/Logic/Diaconescu.mma
@@ -16,23 +16,23 @@
 
 include "Coq.ma".
 
-(*#**********************************************************************)
+(*#***********************************************************************)
 
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
-(*   \VV/  *************************************************************)
+(*   \VV/  **************************************************************)
 
-(*    //   *      This file is distributed under the terms of the      *)
+(*    //   *      This file is distributed under the terms of the       *)
 
-(*         *       GNU Lesser General Public License Version 2.1       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
 
-(*#**********************************************************************)
+(*#***********************************************************************)
 
-(*i $Id: Diaconescu.v,v 1.5 2003/12/24 10:27:05 barras Exp $ i*)
+(*i $Id: Diaconescu.v,v 1.5.2.3 2004/08/01 09:36:44 herbelin Exp $ i*)
 
-(* R. Diaconescu [Diaconescu] showed that the Axiom of Choice in Set Theory
+(*#* R. Diaconescu [Diaconescu] showed that the Axiom of Choice in Set Theory
    entails Excluded-Middle; S. Lacas and B. Werner [LacasWerner]
    adapted the proof to show that the axiom of choice in equivalence
    classes entails Excluded-Middle in Type Theory.
@@ -53,11 +53,11 @@ include "Coq.ma".
 Section PredExt_GuardRelChoice_imp_EM
 *)
 
-(* The axiom of extensionality for predicates *)
+(*#* The axiom of extensionality for predicates *)
 
 inline procedural "cic:/Coq/Logic/Diaconescu/PredicateExtensionality.con" as definition.
 
-(* From predicate extensionality we get propositional extensionality
+(*#* From predicate extensionality we get propositional extensionality
    hence proof-irrelevance *)
 
 include "Logic/ClassicalFacts.ma".
@@ -70,7 +70,7 @@ inline procedural "cic:/Coq/Logic/Diaconescu/prop_ext.con" as lemma.
 
 inline procedural "cic:/Coq/Logic/Diaconescu/proof_irrel.con" as lemma.
 
-(* From proof-irrelevance and relational choice, we get guarded
+(*#* From proof-irrelevance and relational choice, we get guarded
    relational choice *)
 
 include "Logic/ChoiceFacts.ma".
@@ -81,16 +81,16 @@ cic:/Coq/Logic/Diaconescu/PredExt_GuardRelChoice_imp_EM/rel_choice.var
 
 inline procedural "cic:/Coq/Logic/Diaconescu/guarded_rel_choice.con" as lemma.
 
-(* The form of choice we need: there is a functional relation which chooses
-   an element in any non empty subset of bool *)
+(*#* The form of choice we need: there is a functional relation which chooses
+    an element in any non empty subset of bool *)
 
 include "Bool/Bool.ma".
 
 inline procedural "cic:/Coq/Logic/Diaconescu/AC.con" as lemma.
 
-(* The proof of the excluded middle *)
+(*#* The proof of the excluded middle *)
 
-(* Remark: P could have been in Set or Type *)
+(*#* Remark: P could have been in Set or Type *)
 
 inline procedural "cic:/Coq/Logic/Diaconescu/pred_ext_and_rel_choice_imp_EM.con" as theorem.