Ajout exists! et restructuration/extension des fichiers sur la

description et le choix


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8892 85f007b7-540e-0410-9357-904b9bb8a0f7

10 files changed, 999 insertions, 225 deletions

diff --git a/.depend.coq b/.depend.coq
index caa85a2c6..46a2af571 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -106,20 +106,22 @@ theories/Logic/Classical.vo: theories/Logic/Classical.v theories/Logic/Classical
 theories/Logic/Classical_Type.vo: theories/Logic/Classical_Type.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo
 theories/Logic/Classical_Pred_Set.vo: theories/Logic/Classical_Pred_Set.v theories/Logic/Classical_Pred_Type.vo
 theories/Logic/Eqdep.vo: theories/Logic/Eqdep.v theories/Logic/EqdepFacts.vo
-theories/Logic/Classical_Pred_Type.vo: theories/Logic/Classical_Pred_Type.v theories/Logic/Classical_Prop.vo
 theories/Logic/Classical_Prop.vo: theories/Logic/Classical_Prop.v theories/Logic/ClassicalFacts.vo theories/Logic/EqdepFacts.vo
+theories/Logic/Classical_Pred_Type.vo: theories/Logic/Classical_Pred_Type.v theories/Logic/Classical_Prop.vo
 theories/Logic/ClassicalFacts.vo: theories/Logic/ClassicalFacts.v theories/Logic/Hurkens.vo
-theories/Logic/ChoiceFacts.vo: theories/Logic/ChoiceFacts.v theories/Arith/Wf_nat.vo theories/Arith/Compare_dec.vo theories/Logic/Decidable.vo theories/Arith/Arith.vo
+theories/Logic/ChoiceFacts.vo: theories/Logic/ChoiceFacts.v theories/Arith/Wf_nat.vo theories/Arith/Compare_dec.vo theories/Logic/Decidable.vo theories/Arith/Arith.vo theories/Setoids/Setoid.vo
 theories/Logic/Berardi.vo: theories/Logic/Berardi.v
 theories/Logic/Eqdep_dec.vo: theories/Logic/Eqdep_dec.v theories/Logic/EqdepFacts.vo
 theories/Logic/Decidable.vo: theories/Logic/Decidable.v
 theories/Logic/JMeq.vo: theories/Logic/JMeq.v theories/Logic/Eqdep.vo
-theories/Logic/ClassicalDescription.vo: theories/Logic/ClassicalDescription.v theories/Logic/Classical.vo
-theories/Logic/ClassicalChoice.vo: theories/Logic/ClassicalChoice.v theories/Logic/ClassicalDescription.vo theories/Logic/RelationalChoice.vo theories/Logic/ChoiceFacts.vo
+theories/Logic/ClassicalChoice.vo: theories/Logic/ClassicalChoice.v theories/Logic/ClassicalUniqueChoice.vo theories/Logic/RelationalChoice.vo theories/Logic/ChoiceFacts.vo
+theories/Logic/ClassicalDescription.vo: theories/Logic/ClassicalDescription.v theories/Logic/Classical.vo theories/Logic/ChoiceFacts.vo theories/Setoids/Setoid.vo
 theories/Logic/RelationalChoice.vo: theories/Logic/RelationalChoice.v
 theories/Logic/Diaconescu.vo: theories/Logic/Diaconescu.v theories/Logic/ClassicalFacts.vo theories/Logic/ChoiceFacts.vo theories/Bool/Bool.vo
 theories/Logic/EqdepFacts.vo: theories/Logic/EqdepFacts.v
 theories/Logic/ProofIrrelevanceFacts.vo: theories/Logic/ProofIrrelevanceFacts.v theories/Logic/EqdepFacts.vo
+theories/Logic/ClassicalEpsilon.vo: theories/Logic/ClassicalEpsilon.v theories/Logic/Classical.vo theories/Logic/ChoiceFacts.vo
+theories/Logic/ClassicalUniqueChoice.vo: theories/Logic/ClassicalUniqueChoice.v theories/Logic/Classical.vo theories/Setoids/Setoid.vo
 theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/Arith/Factorial.vo
 theories/Arith/Gt.vo: theories/Arith/Gt.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo
 theories/Arith/Between.vo: theories/Arith/Between.v theories/Arith/Le.vo theories/Arith/Lt.vo
@@ -240,8 +242,6 @@ theories/FSets/FMapPositive.vo: theories/FSets/FMapPositive.v theories/ZArith/ZA
 theories/FSets/FMapIntMap.vo: theories/FSets/FMapIntMap.v theories/Bool/Bool.vo theories/NArith/NArith.vo theories/NArith/Ndigits.vo theories/NArith/Ndec.vo theories/NArith/Nnat.vo theories/IntMap/Allmaps.vo theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo
 theories/FSets/FSetToFiniteSet.vo: theories/FSets/FSetToFiniteSet.v theories/Sets/Ensembles.vo theories/Sets/Finite_sets.vo theories/FSets/FSetInterface.vo theories/FSets/FSetProperties.vo theories/FSets/OrderedTypeEx.vo
 theories/FSets/Int.vo: theories/FSets/Int.v theories/ZArith/ZArith.vo contrib/romega/ROmega.vo
-theories/FSets/FMapAVL.vo: theories/FSets/FMapAVL.v theories/FSets/FSetInterface.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo theories/ZArith/ZArith.vo theories/FSets/Int.vo
-theories/FSets/FSetAVL.vo: theories/FSets/FSetAVL.v theories/FSets/FSetInterface.vo theories/FSets/FSetList.vo theories/ZArith/ZArith.vo theories/FSets/Int.vo
 theories/IntMap/Adalloc.vo: theories/IntMap/Adalloc.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/NArith/NArith.vo theories/NArith/Ndigits.vo theories/NArith/Ndec.vo theories/NArith/Nnat.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo
 theories/IntMap/Mapcanon.vo: theories/IntMap/Mapcanon.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/NArith/NArith.vo theories/NArith/Ndigits.vo theories/NArith/Ndec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Fset.vo theories/Lists/List.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/IntMap/Mapcard.vo
 theories/IntMap/Mapfold.vo: theories/IntMap/Mapfold.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/NArith/NArith.vo theories/NArith/Ndigits.vo theories/NArith/Ndec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/Lists/List.vo
@@ -275,6 +275,54 @@ theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith_base.
 theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo contrib/field/Field.vo
 theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/RIneq.vo contrib/omega/Omega.vo
 theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo theories/Reals/DiscrR.vo
+theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo
+theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo contrib/fourier/Fourier.vo
+theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo
+theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo
+theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/Rbase.vo
+theories/Reals/ArithProp.vo: theories/Reals/ArithProp.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Arith/Even.vo theories/Arith/Div2.vo
+theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo
+theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical.vo theories/Arith/Compare.vo
+theories/Reals/SeqProp.vo: theories/Reals/SeqProp.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Logic/Classical.vo theories/Arith/Max.vo
+theories/Reals/Rcomplete.vo: theories/Reals/Rcomplete.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Arith/Max.vo
+theories/Reals/PartSum.vo: theories/Reals/PartSum.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/Rcomplete.vo theories/Arith/Max.vo
+theories/Reals/AltSeries.vo: theories/Reals/AltSeries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo
+theories/Reals/Binomial.vo: theories/Reals/Binomial.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/PartSum.vo
+theories/Reals/Rsigma.vo: theories/Reals/Rsigma.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo
+theories/Reals/Rprod.vo: theories/Reals/Rprod.v theories/Arith/Compare.vo theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo theories/Reals/Binomial.vo
+theories/Reals/Cauchy_prod.vo: theories/Reals/Cauchy_prod.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo
+theories/Reals/Alembert.vo: theories/Reals/Alembert.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo
+theories/Reals/SeqSeries.vo: theories/Reals/SeqSeries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Arith/Max.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/Rcomplete.vo theories/Reals/PartSum.vo theories/Reals/AltSeries.vo theories/Reals/Binomial.vo theories/Reals/Rsigma.vo theories/Reals/Rprod.vo theories/Reals/Cauchy_prod.vo theories/Reals/Alembert.vo
+theories/Reals/Rtrigo_fun.vo: theories/Reals/Rtrigo_fun.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo
+theories/Reals/Rtrigo_def.vo: theories/Reals/Rtrigo_def.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Arith/Max.vo
+theories/Reals/Rtrigo_alt.vo: theories/Reals/Rtrigo_alt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo
+theories/Reals/Cos_rel.vo: theories/Reals/Cos_rel.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo
+theories/Reals/Cos_plus.vo: theories/Reals/Cos_plus.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo theories/Reals/Cos_rel.vo theories/Arith/Max.vo
+theories/Reals/Rtrigo.vo: theories/Reals/Rtrigo.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_rel.vo theories/Reals/Cos_plus.vo theories/ZArith/ZArith_base.vo theories/ZArith/Zcomplements.vo theories/Logic/Classical_Prop.vo
+theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical_Prop.vo contrib/fourier/Fourier.vo
+theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo contrib/fourier/Fourier.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo
+theories/Reals/RList.vo: theories/Reals/RList.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo
+theories/Reals/Ranalysis1.vo: theories/Reals/Ranalysis1.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo
+theories/Reals/Ranalysis2.vo: theories/Reals/Ranalysis2.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo
+theories/Reals/Ranalysis3.vo: theories/Reals/Ranalysis3.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo
+theories/Reals/Rtopology.vo: theories/Reals/Rtopology.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/RList.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo
+theories/Reals/MVT.vo: theories/Reals/MVT.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Rtopology.vo
+theories/Reals/PSeries_reg.vo: theories/Reals/PSeries_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Arith/Max.vo theories/Arith/Even.vo
+theories/Reals/Exp_prop.vo: theories/Reals/Exp_prop.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo theories/Arith/Div2.vo theories/Arith/Even.vo theories/Arith/Max.vo
+theories/Reals/Rtrigo_reg.vo: theories/Reals/Rtrigo_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo
+theories/Reals/Rsqrt_def.vo: theories/Reals/Rsqrt_def.v theories/Bool/Sumbool.vo theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo
+theories/Reals/R_sqrt.vo: theories/Reals/R_sqrt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rsqrt_def.vo
+theories/Reals/Rtrigo_calc.vo: theories/Reals/Rtrigo_calc.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo
+theories/Reals/Rgeom.vo: theories/Reals/Rgeom.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo
+theories/Reals/Sqrt_reg.vo: theories/Reals/Sqrt_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo
+theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis3.vo theories/Reals/Exp_prop.vo
+theories/Reals/Rpower.vo: theories/Reals/Rpower.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Exp_prop.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/MVT.vo theories/Reals/Ranalysis4.vo
+theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Rtopology.vo theories/Reals/MVT.vo theories/Reals/PSeries_reg.vo theories/Reals/Exp_prop.vo theories/Reals/Rtrigo_reg.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/Rtrigo_calc.vo theories/Reals/Rgeom.vo theories/Reals/RList.vo theories/Reals/Sqrt_reg.vo theories/Reals/Ranalysis4.vo theories/Reals/Rpower.vo
+theories/Reals/NewtonInt.vo: theories/Reals/NewtonInt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo
+theories/Reals/RiemannInt_SF.vo: theories/Reals/RiemannInt_SF.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis.vo theories/Logic/Classical_Prop.vo
+theories/Reals/RiemannInt.vo: theories/Reals/RiemannInt.v theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis.vo theories/Reals/Rbase.vo theories/Reals/RiemannInt_SF.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo theories/Arith/Max.vo
+theories/Reals/Integration.vo: theories/Reals/Integration.v theories/Reals/NewtonInt.vo theories/Reals/RiemannInt_SF.vo theories/Reals/RiemannInt.vo
+theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo theories/Reals/Integration.vo
 theories/Sorting/Heap.vo: theories/Sorting/Heap.v theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo theories/Sorting/Sorting.vo
 theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v theories/Relations/Relations.vo theories/Lists/List.vo theories/Sets/Multiset.vo theories/Arith/Arith.vo
 theories/Sorting/Sorting.vo: theories/Sorting/Sorting.v theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo
diff --git a/Makefile b/Makefile
index 526fdf1e5..d446d5f7f 100644
--- a/Makefile
+++ b/Makefile
@@ -813,16 +813,17 @@ INITVO=\
 init: $(INITVO)
 
 LOGICVO=\
- theories/Logic/Hurkens.vo          	theories/Logic/ProofIrrelevance.vo\
- theories/Logic/Classical.vo          	theories/Logic/Classical_Type.vo \
- theories/Logic/Classical_Pred_Set.vo   theories/Logic/Eqdep.vo          \
- theories/Logic/Classical_Pred_Type.vo  theories/Logic/Classical_Prop.vo \
- theories/Logic/ClassicalFacts.vo       theories/Logic/ChoiceFacts.vo \
- theories/Logic/Berardi.vo       	theories/Logic/Eqdep_dec.vo \
- theories/Logic/Decidable.vo            theories/Logic/JMeq.vo \
- theories/Logic/ClassicalDescription.vo theories/Logic/ClassicalChoice.vo \
- theories/Logic/RelationalChoice.vo     theories/Logic/Diaconescu.vo \
- theories/Logic/EqdepFacts.vo           theories/Logic/ProofIrrelevanceFacts.vo
+ theories/Logic/Hurkens.vo            theories/Logic/ProofIrrelevance.vo\
+ theories/Logic/Classical.vo          theories/Logic/Classical_Type.vo \
+ theories/Logic/Classical_Pred_Set.vo theories/Logic/Eqdep.vo          \
+ theories/Logic/Classical_Prop.vo     theories/Logic/Classical_Pred_Type.vo \
+ theories/Logic/ClassicalFacts.vo     theories/Logic/ChoiceFacts.vo \
+ theories/Logic/Berardi.vo            theories/Logic/Eqdep_dec.vo \
+ theories/Logic/Decidable.vo          theories/Logic/JMeq.vo \
+ theories/Logic/ClassicalChoice.vo    theories/Logic/ClassicalDescription.vo \
+ theories/Logic/RelationalChoice.vo   theories/Logic/Diaconescu.vo \
+ theories/Logic/EqdepFacts.vo         theories/Logic/ProofIrrelevanceFacts.vo \
+ theories/Logic/ClassicalEpsilon.vo   theories/Logic/ClassicalUniqueChoice.vo 
 
 ARITHVO=\
  theories/Arith/Arith.vo        theories/Arith/Gt.vo          \
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 4907c93a4..53a526895 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -280,13 +280,35 @@ Qed.
 
 Hint Immediate sym_eq sym_not_eq: core v62.
 
-(** Other notations *)
+(** Basic definitions about relations and properties *)
 
-Notation "'exists' ! x , P" := 
-  (exists x',  (fun x => P) x' /\ forall x'', (fun x => P) x'' -> x' = x'')
+Definition subrelation (A B : Type) (R R' : A->B->Prop) :=
+  forall x y, R x y -> R' x y.
+
+Definition singleton (A : Type) (P : A->Prop) (x:A) :=
+  P x /\ forall (x':A), P x' -> x=x'.
+
+Definition uniqueness (A:Type) (P:A->Prop) := forall x y, P x -> P y -> x = y.
+
+(** Unique existence *)
+
+Notation "'exists' ! x , P" := (exists x', singleton (fun x => P) x')
   (at level 200, x ident, right associativity,
    format "'[' 'exists' !  '/  ' x ,  '/  ' P ']'") : type_scope.
-Notation "'exists' ! x : A , P" := 
-  (exists x' : A,  (fun x => P) x' /\ forall x'':A, (fun x => P) x'' -> x' = x'')
+Notation "'exists' ! x : A , P" := (exists x':A, singleton (fun x:A => P) x')
   (at level 200, x ident, right associativity,
    format "'[' 'exists' !  '/  ' x  :  A ,  '/  ' P ']'") : type_scope.
+
+Lemma unique_existence : forall (A:Type) (P:A->Prop),
+  ((exists x, P x) /\ uniqueness P) <-> (exists! x, P x).
+Proof.
+intros A P; split.
+  intros ((x,Hx),Huni); exists x; red; auto.
+  intros (x,(Hx,Huni)); split. 
+    exists x; assumption.
+    intros x' x'' Hx' Hx''; transitivity x.
+      symmetry; auto.
+      auto.
+Qed.
+
+
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 5180bf5b2..71db456e9 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -8,153 +9,451 @@
 
 (*i $Id$ i*)
 
-(** We show that the functional formulation of the axiom of Choice
-   (usual formulation in type theory) is equivalent to its relational
-   formulation (only formulation of set theory) + the axiom of
-   (parametric) definite description (aka axiom of unique choice) *)
+(** ** Some facts and definitions concerning choice and description in
+       intuitionistic logic.
 
-(** This shows that the axiom of choice can be assumed (under its
-   relational formulation) without known inconsistency with classical logic,
-   though definite description conflicts with classical logic *)
+We investigate the relations between the following choice and
+description principles
+
+- AC_rel  = relational form of the (non extensional) axiom of choice
+            (a "set-theoretic" axiom of choice)
+- AC_fun  = functional form of the (non extensional) axiom of choice
+            (a "type-theoretic" axiom of choice)
+- AC!     = functional relation reification
+            (known as axiom of unique choice in topos theory,
+             sometimes called principle of definite description in 
+             the context of constructive type theory)
+
+- GAC_rel = guarded relational form of the (non extensional) axiom of choice
+- GAC_fun = guarded functional form of the (non extensional) axiom of choice
+- GAC!    = guarded functional relation reification
+
+- OAC_rel = "omniscient" relational form of the (non extensional) axiom of choice
+- OAC_fun = "omniscient" functional form of the (non extensional) axiom of choice
+            (called AC* in Bell [Bell])
+- OAC!
+
+- ID_iota    = intuitionistic definite description
+- ID_epsilon = intuitionistic indefinite description
+
+- D_iota     = (weakly classical) definite description principle
+- D_epsilon  = (weakly classical) indefinite description principle
+
+- PI      = proof irrelevance
+- IGP     = independence of general premises
+            (an unconstrained generalisation of the constructive principle of
+             independence of premises)
+- Drinker = drinker's paradox (small form)
+            (called Ex in Bell [Bell])  
+
+We let also
+
+IPL_2^2 = 2nd-order impredicative, 2nd-order functional minimal predicate logic
+IPL_2   = 2nd-order impredicative minimal predicate logic
+IPL^2   = 2nd-order functional minimal predicate logic (with ex. quant.)
+
+Table of contents
+
+A. Definitions
+
+B. IPL_2^2 |- AC_rel + AC! = AC_fun
+
+C. 1. AC_rel + PI -> GAC_rel  and  PL_2 |- AC_rel + IGP -> GAC_rel and GAC_rel = OAC_rel
+
+C. 2. IPL^2 |- AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker
+
+D. Derivability of choice for decidable relations with well-ordered codomain
+
+E. Equivalence of choices on dependent or non dependent functional types
+
+F. Non contradiction of constructive descriptions wrt functional choices
+
+G. Definite description transports classical logic to the computational world
 
-Section ChoiceEquivalences.
+References:
+
+[Bell] John L. Bell, Choice principles in intuitionistic set theory,
+unpublished.
+
+[Bell93] John L. Bell, Hilbert's Epsilon Operator in Intuitionistic
+Type Theories, Mathematical Logic Quarterly, volume 39, 1993.
+
+[Carlstrøm05] Jesper Carlstrøm, Interpreting descriptions in
+intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005.
+*)
+
+Set Implicit Arguments.
+
+Notation Local "'inhabited' A" := A (at level 10, only parsing).
+
+(**********************************************************************)
+(** *** A. Definitions *)
+
+(** Choice, reification and description schemes *)
+
+Section ChoiceSchemes.
 
 Variables A B :Type.
 
-Definition RelationalChoice :=
-  forall (R:A -> B -> Prop),
-    (forall x:A, exists y : B, R x y) ->
-     exists R' : A -> B -> Prop,
-      (forall x:A,
-         exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
+Variables P:A->Prop.
+
+Variables R:A->B->Prop.
+
+(** **** Constructive choice and description *)
+
+(** AC_rel *)
+
+Definition RelationalChoice_on :=
+  forall R:A->B->Prop,
+  (forall x : A, exists y : B, R x y) ->
+  (exists R' : A->B->Prop, subrelation R' R /\ forall x, exists! y, R' x y).
+
+(** AC_fun *)
+
+Definition FunctionalChoice_on :=
+  forall R:A->B->Prop,
+  (forall x : A, exists y : B, R x y) ->
+  (exists f : A->B, forall x : A, R x (f x)).
+
+(** AC! or Functional Relation Reification (known as Axiom of Unique Choice
+    in topos theory; also called principle of definite description *)
+
+Definition FunctionalRelReification_on :=
+  forall R:A->B->Prop,
+  (forall x : A, exists! y : B, R x y) ->
+  (exists f : A->B, forall x : A, R x (f x)).
+
+(** ID_epsilon (constructive version of indefinite description;
+    combined with proof-irrelevance, it may be connected to
+    Carlstrøm's type theory with a constructive indefinite description
+    operator) *)
+
+Definition ConstructiveIndefiniteDescription_on :=
+  forall P:A->Prop,
+  (exists x, P x) -> { x:A | P x }.
+
+(** ID_iota (constructive version of definite description; combined
+    with proof-irrelevance, it may be connected to Carlstrøm's and
+    Stenlund's type theory with a constructive definite description
+    operator) *)
+
+Definition ConstructiveDefiniteDescription_on :=
+  forall P:A->Prop,
+  (exists! x, P x) -> { x:A | P x }.
+
+(** **** Weakly classical choice and description *)
 
-Definition FunctionalChoice :=
-  forall (R:A -> B -> Prop),
-    (forall x:A, exists y : B, R x y) ->
-     exists f : A -> B, (forall x:A, R x (f x)).
+(** GAC_rel *)
 
-Definition ParamDefiniteDescription :=
-  forall (R:A -> B -> Prop),
-    (forall x:A, exists y : B, R x y /\ (forall y':B, R x y' -> y = y')) ->
-     exists f : A -> B, (forall x:A, R x (f x)).
+Definition GuardedRelationalChoice_on := 
+  forall P : A->Prop, forall R : A->B->Prop,
+  (forall x : A, P x -> exists y : B, R x y) ->
+  (exists R' : A->B->Prop, 
+     subrelation R' R /\ forall x, P x -> exists! y, R' x y).
+
+(** GAC_fun *)
+
+Definition GuardedFunctionalChoice_on := 
+  forall P : A->Prop, forall R : A->B->Prop, 
+  inhabited B ->
+  (forall x : A, P x -> exists y : B, R x y) ->
+  (exists f : A->B, forall x, P x -> R x (f x)).
+
+(** GFR_fun *)
+
+Definition GuardedFunctionalRelReification_on :=
+  forall P : A->Prop, forall R : A->B->Prop, 
+  inhabited B ->
+  (forall x : A, P x -> exists! y : B, R x y) ->
+  (exists f : A->B, forall x : A, P x -> R x (f x)).
+
+(** OAC_rel *)
+
+Definition OmniscientRelationalChoice_on := 
+  forall R : A->B->Prop,
+  exists R' : A->B->Prop, 
+    subrelation R' R /\ forall x : A, (exists y : B, R x y) -> exists! y, R' x y.
+
+(** OAC_fun *)
+
+Definition OmniscientFunctionalChoice_on := 
+  forall R : A->B->Prop, 
+  inhabited B ->
+  exists f : A->B, forall x : A, (exists y : B, R x y) -> R x (f x).
+
+(** D_epsilon *)
+
+Definition ClassicalIndefiniteDescription := 
+  forall P:A->Prop,
+  A -> { x:A | (exists x, P x) -> P x }.
+
+(** D_iota *)
+
+Definition ClassicalDefiniteDescription := 
+  forall P:A->Prop,
+  A -> { x:A | (exists! x, P x) -> P x }.
+
+End ChoiceSchemes.
+
+(** Generalized schemes *)
+
+Notation RelationalChoice :=
+  (forall A B, RelationalChoice_on A B).
+Notation FunctionalChoice :=
+  (forall A B, FunctionalChoice_on A B).
+Notation FunctionalChoiceOnInhabitedSet :=
+  (forall A B, inhabited B -> FunctionalChoice_on A B).
+Notation FunctionalRelReification :=
+  (forall A B, FunctionalRelReification_on A B).
+
+Notation GuardedRelationalChoice := 
+  (forall A B, GuardedRelationalChoice_on A B).
+Notation GuardedFunctionalChoice :=
+  (forall A B, GuardedFunctionalChoice_on A B).
+Notation GuardedFunctionalRelReification :=
+  (forall A B, GuardedFunctionalRelReification_on A B).
+
+Notation OmniscientRelationalChoice :=
+  (forall A B, OmniscientRelationalChoice_on A B).
+Notation OmniscientFunctionalChoice :=
+  (forall A B, OmniscientFunctionalChoice_on A B).
+
+Notation ConstructiveDefiniteDescription := 
+  (forall A, ConstructiveDefiniteDescription_on A).
+Notation ConstructiveIndefiniteDescription := 
+  (forall A, ConstructiveIndefiniteDescription_on A).
+
+(** Subclassical schemes *)
+
+Definition ProofIrrelevance :=
+  forall (A:Prop) (a1 a2:A), a1 = a2.
+
+Definition IndependenceOfGeneralPremises :=
+  forall (A:Type) (P:A -> Prop) (Q:Prop), 
+    inhabited A ->
+    (Q -> exists x, P x) -> exists x, Q -> P x.
+
+Definition SmallDrinker'sParadox :=
+  forall (A:Type) (P:A -> Prop), inhabited A ->
+  exists x, (exists x, P x) -> P x.
+
+(**********************************************************************)
+(** *** B. AC_rel + PDP = AC_fun
+
+   We show that the functional formulation of the axiom of Choice
+   (usual formulation in type theory) is equivalent to its relational
+   formulation (only formulation of set theory) + the axiom of
+   (parametric) definite description (aka axiom of unique choice) *)
+
+(** This shows that the axiom of choice can be assumed (under its
+   relational formulation) without known inconsistency with classical logic,
+   though definite description conflicts with classical logic *)
 
 Lemma description_rel_choice_imp_funct_choice :
- ParamDefiniteDescription -> RelationalChoice -> FunctionalChoice.
-intros Descr RelCh.
-red in |- *; intros R H.
-destruct (RelCh R H) as [R' H0].
-destruct (Descr R') as [f H1].
-intro x.
-elim (H0 x); intros y [H2 [H3 H4]]; exists y; split; [ exact H3 | exact H4 ].
+  forall A B : Type,
+  FunctionalRelReification_on A B -> RelationalChoice_on A B -> FunctionalChoice_on A B.
+Proof.
+intros A B Descr RelCh R H.
+destruct (RelCh R H) as (R',(HR'R,H0)).
+destruct (Descr R') as (f,Hf).
+firstorder.
 exists f; intro x.
-elim (H0 x); intros y [H2 [H3 H4]].
-rewrite <- (H4 (f x) (H1 x)).
-exact H2.
+destruct (H0 x) as (y,(HR'xy,Huniq)).
+rewrite <- (Huniq (f x) (Hf x)).
+apply HR'R; assumption.
 Qed.
 
-Lemma funct_choice_imp_rel_choice : FunctionalChoice -> RelationalChoice.
-intros FunCh.
-red in |- *; intros R H.
-destruct (FunCh R H) as [f H0].
-exists (fun x y => y = f x).
-intro x; exists (f x); split;
- [ apply H0
- | split; [ reflexivity | intros y H1; symmetry  in |- *; exact H1 ] ].
+Lemma funct_choice_imp_rel_choice : 
+  forall A B, FunctionalChoice_on A B -> RelationalChoice_on A B.
+Proof.
+intros A B FunCh R H.
+destruct (FunCh R H) as (f,H0).
+exists (fun x y => f x = y).
+split.
+  intros x y Heq; rewrite <- Heq; trivial.
+  intro x; exists (f x); split.
+    reflexivity.
+    trivial.
 Qed.
 
-Lemma funct_choice_imp_description :
- FunctionalChoice -> ParamDefiniteDescription.
-intros FunCh.
-red in |- *; intros R H.
+Lemma funct_choice_imp_description : 
+  forall A B, FunctionalChoice_on A B -> FunctionalRelReification_on A B.
+Proof.
+intros A B FunCh R H.
 destruct (FunCh R) as [f H0].
 (* 1 *)
 intro x.
-elim (H x); intros y [H0 H1].
-exists y; exact H0.
+destruct (H x) as (y,(HRxy,_)).
+exists y; exact HRxy.
 (* 2 *)
 exists f; exact H0.
 Qed.
 
 Theorem FunChoice_Equiv_RelChoice_and_ParamDefinDescr :
- FunctionalChoice <-> RelationalChoice /\ ParamDefiniteDescription.
-split.
+  forall A B, FunctionalChoice_on A B <-> 
+    RelationalChoice_on A B /\ FunctionalRelReification_on A B.
+Proof.
+intros A B; split.
 intro H; split;
  [ exact (funct_choice_imp_rel_choice H)
  | exact (funct_choice_imp_description H) ].
 intros [H H0]; exact (description_rel_choice_imp_funct_choice H0 H).
 Qed.
 
-End ChoiceEquivalences.
+(**********************************************************************)
+(** *** C. Connection between the guarded, non guarded and descriptive choices and *)
 
 (** We show that the guarded relational formulation of the axiom of Choice
    comes from the non guarded formulation in presence either of the
    independance of premises or proof-irrelevance *)
 
-Definition GuardedRelationalChoice (A B:Type) :=
-  forall (P:A -> Prop) (R:A -> B -> Prop),
-    (forall x:A, P x -> exists y : B, R x y) ->
-     exists R' : A -> B -> Prop,
-      (forall x:A,
-         P x ->
-         exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
-
-Definition ProofIrrelevance := forall (A:Prop) (a1 a2:A), a1 = a2.
+(**********************************************************************)
+(** **** C. 1. AC_rel + PI -> GAC_rel and AC_rel + IGP -> GAC_rel and GAC_rel = OAC_rel *)
 
 Lemma rel_choice_and_proof_irrel_imp_guarded_rel_choice :
-  (forall A B, RelationalChoice A B)
-    -> ProofIrrelevance -> (forall A B, GuardedRelationalChoice A B).
+  RelationalChoice -> ProofIrrelevance -> GuardedRelationalChoice.
 Proof.
 intros rel_choice proof_irrel.
 red in |- *; intros A B P R H.
-destruct (rel_choice _ _ (fun (x:sigT P) (y:B) => R (projT1 x) y)) as [R' H0].
-intros [x HPx].
-destruct (H x HPx) as [y HRxy].
+destruct (rel_choice _ _ (fun (x:sigT P) (y:B) => R (projT1 x) y)) as (R',(HR'R,H0)).
+intros (x,HPx).
+destruct (H x HPx) as (y,HRxy).
 exists y; exact HRxy.
 set (R'' := fun (x:A) (y:B) => exists H : P x, R' (existT P x H) y).
-exists R''; intros x HPx.
-destruct (H0 (existT P x HPx)) as [y [HRxy [HR'xy Huniq]]].
-exists y. split.
-  exact HRxy.
-  split.
-    red in |- *; exists HPx; exact HR'xy.
-    intros y' HR''xy'.
+exists R''; split.
+  intros x y (HPx,HR'xy).
+    change x with (projT1 (existT P x HPx)); apply HR'R; exact HR'xy.
+  intros x HPx.
+  destruct (H0 (existT P x HPx)) as (y,(HR'xy,Huniq)).
+    exists y; split. exists HPx; exact HR'xy.
+    intros y' (H'Px,HR'xy').
       apply Huniq.
-      unfold R'' in HR''xy'.
-      destruct HR''xy' as [H'Px HR'xy'].
-      rewrite proof_irrel with (a1 := HPx) (a2 := H'Px).
-      exact HR'xy'.
+      rewrite proof_irrel with (a1 := HPx) (a2 := H'Px); exact HR'xy'.
 Qed.
 
-Definition IndependenceOfGeneralPremises :=
-  forall (A:Type) (P:A -> Prop) (Q:Prop),
-    (Q -> exists x, P x) -> exists x, Q -> P x.
-
 Lemma rel_choice_indep_of_general_premises_imp_guarded_rel_choice :
- forall A B, RelationalChoice A B -> 
-   IndependenceOfGeneralPremises -> GuardedRelationalChoice A B.
-Proof.
-intros A B RelCh IndPrem.
-red in |- *; intros P R H.
-destruct (RelCh (fun x y => P x -> R x y)) as [R' H0].
-  intro x. apply IndPrem.
-    apply H.
-  exists R'.
-  intros x HPx.
-    destruct (H0 x) as [y [H1 H2]].
-    exists y. split. 
-      apply (H1 HPx).
-      exact H2.
+ forall A B, inhabited B -> RelationalChoice_on A B -> 
+  IndependenceOfGeneralPremises -> GuardedRelationalChoice_on A B.
+Proof.
+intros A B Inh AC_rel IndPrem P R H.
+destruct (AC_rel (fun x y => P x -> R x y)) as (R',(HR'R,H0)).
+  intro x. apply IndPrem. exact Inh. intro Hx. 
+    apply H; assumption.
+  exists (fun x y => P x /\ R' x y).
+  firstorder.
+Qed.
+
+Lemma guarded_rel_choice_imp_rel_choice :
+ forall A B, GuardedRelationalChoice_on A B -> RelationalChoice_on A B.
+Proof.
+intros A B GAC_rel R H.
+destruct (GAC_rel (fun _ => True) R) as (R',(HR'R,H0)).
+  firstorder.
+exists R'; firstorder.
 Qed.
 
+(** OAC_rel = GAC_rel *)
+
+Lemma guarded_iff_omniscient_rel_choice :
+  GuardedRelationalChoice <-> OmniscientRelationalChoice.
+Proof.
+split.
+  intros GAC_rel A B R.
+    apply (GAC_rel A B (fun x => exists y, R x y) R); auto.
+  intros OAC_rel A B P R H.
+    destruct (OAC_rel A B R) as (f,Hf); exists f; firstorder.
+Qed.
+
+(**********************************************************************)
+(** **** C. 2. AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker *)
+
+(** AC_fun + IGP = GAC_fun *)
+ 
+Lemma guarded_fun_choice_imp_indep_of_general_premises :
+ GuardedFunctionalChoice -> IndependenceOfGeneralPremises.
+Proof.
+intros GAC_fun A P Q Inh H.
+destruct (GAC_fun unit A (fun _ => Q) (fun _ => P) Inh) as (f,Hf).
+tauto.
+exists (f tt); auto.
+Qed.
+
+Lemma guarded_fun_choice_imp_fun_choice :
+ GuardedFunctionalChoice -> FunctionalChoiceOnInhabitedSet.
+Proof.
+intros GAC_fun A B Inh R H.
+destruct (GAC_fun A B (fun _ => True) R Inh) as (f,Hf).
+firstorder.
+exists f; auto.
+Qed.
+
+Lemma fun_choice_and_indep_general_prem_imp_guarded_fun_choice :
+  FunctionalChoiceOnInhabitedSet -> IndependenceOfGeneralPremises
+  -> GuardedFunctionalChoice.
+Proof.
+intros AC_fun IndPrem A B P R Inh H.
+apply (AC_fun A B Inh (fun x y => P x -> R x y)).
+intro x; apply IndPrem; eauto.
+Qed.
+
+(** AC_fun + Drinker = OAC_fun *)
+
+(** This was already observed by Bell [Bell] *)
+
+Lemma omniscient_fun_choice_imp_small_drinker :
+  OmniscientFunctionalChoice -> SmallDrinker'sParadox.
+Proof.
+intros OAC_fun A P Inh.
+destruct (OAC_fun unit A (fun _ => P)) as (f,Hf).
+auto.
+exists (f tt); firstorder.
+Qed.
+
+Lemma omniscient_fun_choice_imp_fun_choice :
+  OmniscientFunctionalChoice -> FunctionalChoiceOnInhabitedSet.
+Proof.
+intros OAC_fun A B Inh R H.
+destruct (OAC_fun A B R Inh) as (f,Hf).
+exists f; firstorder.
+Qed.
+
+Lemma fun_choice_and_small_drinker_imp_omniscient_fun_choice :
+  FunctionalChoiceOnInhabitedSet -> SmallDrinker'sParadox 
+  -> OmniscientFunctionalChoice.
+Proof.
+intros AC_fun Drinker A B R Inh.
+destruct (AC_fun A B Inh (fun x y => (exists y, R x y) -> R x y)) as (f,Hf).
+  intro x; apply (Drinker B (R x) Inh).
+  exists f; assumption.
+Qed.
+
+(** OAC_fun = GAC_fun *)
+
+(** This is derivable from the intuitionistic equivalence between IGP and Drinker
+but we give a direct proof *)
+
+Lemma guarded_iff_omniscient_fun_choice :
+  GuardedFunctionalChoice <-> OmniscientFunctionalChoice.
+Proof.
+split.
+  intros GAC_fun A B R Inh.
+    apply (GAC_fun A B (fun x => exists y, R x y) R); auto.
+  intros OAC_fun A B P R Inh H.
+    destruct (OAC_fun A B R Inh) as (f,Hf).
+ exists f; firstorder.
+Qed.
+
+(**********************************************************************)
+(** *** D. Derivability of choice for decidable relations with well-ordered codomain *)
 
 (** Countable codomains, such as [nat], can be equipped with a
     well-order, which implies the existence of a least element on
     inhabited decidable subsets. As a consequence, the relational form of
     the axiom of choice is derivable on [nat] for decidable relations.
 
-    We show instead that definite description and the functional form
-    of the axiom of choice are equivalent on decidable relation with [nat]
-    as codomain 
+    We show instead that functional relation reification and the
+    functional form of the axiom of choice are equivalent on decidable
+    relation with [nat] as codomain 
 *)
 
 Require Import Wf_nat.
@@ -163,12 +462,11 @@ Require Import Decidable.
 Require Import Arith.
 
 Definition has_unique_least_element (A:Type) (R:A->A->Prop) (P:A->Prop) :=
-  (exists x, (P x /\ forall x', P x' -> R x x')
-      /\ forall x', P x' /\ (forall x'', P x'' -> R x' x'') -> x=x').
+  exists! x, P x /\ forall x', P x' -> R x x'.
 
 Lemma dec_inh_nat_subset_has_unique_least_element :
   forall P:nat->Prop, (forall n, P n \/ ~ P n) ->
-    (exists n, P n) -> has_unique_least_element nat le P.
+    (exists n, P n) -> has_unique_least_element le P.
 Proof.
 intros P Pdec (n0,HPn0).
 assert
@@ -194,30 +492,228 @@ assert
   assumption.
   destruct H0.
   rewrite Heqn; assumption.
-destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0];
-  repeat split; 
+  destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0];
+  repeat split;
   assumption || intros n' (HPn',Hminn'); apply le_antisym; auto.
 Qed.
 
-Definition FunctionalChoice_on (A B:Type) (R:A->B->Prop) :=
-    (forall x:A, exists y : B, R x y) ->
-     exists f : A -> B, (forall x:A, R x (f x)).
+Definition FunctionalChoice_on_rel (A B:Type) (R:A->B->Prop) :=
+  (forall x:A, exists y : B, R x y) ->
+   exists f : A -> B, (forall x:A, R x (f x)).
 
 Lemma classical_denumerable_description_imp_fun_choice : 
   forall A:Type, 
-  ParamDefiniteDescription A nat -> 
-  forall R, (forall x y, decidable (R x y)) -> FunctionalChoice_on A nat R.
+  FunctionalRelReification_on A nat -> 
+  forall R:A->nat->Prop, 
+    (forall x y, decidable (R x y)) -> FunctionalChoice_on_rel R.
 Proof.
 intros A Descr.
 red in |- *; intros R Rdec H.
 set (R':= fun x y => R x y /\ forall y', R x y' -> y <= y').
-destruct (Descr R') as [f Hf].
+destruct (Descr R') as (f,Hf).
   intro x.
   apply (dec_inh_nat_subset_has_unique_least_element (R x)). 
     apply Rdec.
     apply (H x).
 exists f.
 intros x.
-destruct (Hf x) as [Hfx _].
+destruct (Hf x) as (Hfx,_).
+assumption.
+Qed.
+
+(**********************************************************************)
+(** *** E. Choice on dependent and non dependent function types are equivalent *)
+
+(** **** E. 1. Choice on dependent and non dependent function types are equivalent *)
+
+Definition DependentFunctionalChoice_on (A:Type) (B:A -> Type) :=
+  forall R:forall x:A, B x -> Prop,
+  (forall x:A, exists y : B x, R x y) ->
+  (exists f : (forall x:A, B x), forall x:A, R x (f x)).
+
+Notation DependentFunctionalChoice := 
+  (forall A (B:A->Type), DependentFunctionalChoice_on B).
+
+(** The easy part *)
+
+Theorem dep_non_dep_functional_choice : 
+  DependentFunctionalChoice -> FunctionalChoice.
+Proof.
+intros AC_depfun A B R H.
+  destruct (AC_depfun A (fun _ => B) R H) as (f,Hf).
+  exists f; trivial.
+Qed.
+
+(** Deriving choice on product types requires some computation on
+    singleton propositional types, so we need computational
+    conjunction projections and dependent elimination of conjunction
+    and equality *)
+
+Scheme and_indd := Induction for and Sort Prop.
+Scheme eq_indd := Induction for eq Sort Prop.
+
+Definition proj1_inf (A B:Prop) (p : A/\B) :=
+  let (a,b) := p in a.
+
+Theorem non_dep_dep_functional_choice : 
+  FunctionalChoice -> DependentFunctionalChoice.
+Proof.
+intros AC_fun A B R H.
+pose (B' := { x:A & B x }). 
+pose (R' := fun (x:A) (y:B') => projT1 y = x /\ R (projT1 y) (projT2 y)). 
+destruct (AC_fun A B' R') as (f,Hf).
+intros x. destruct (H x) as (y,Hy).
+exists (existT (fun x => B x) x y). split; trivial.
+exists (fun x => eq_rect _ _ (projT2 (f x)) _ (proj1_inf (Hf x))).
+intro x; destruct (Hf x) as (Heq,HR) using and_indd.
+destruct (f x); simpl in *.
+destruct Heq using eq_indd; trivial.
+Qed.
+
+(** **** E. 2. Reification of dependent and non dependent functional relation  are equivalent *)
+
+Definition DependentFunctionalRelReification_on (A:Type) (B:A -> Type) :=
+  forall (R:forall x:A, B x -> Prop),
+  (forall x:A, exists! y : B x, R x y) ->
+  (exists f : (forall x:A, B x), forall x:A, R x (f x)).
+
+Notation DependentFunctionalRelReification :=
+  (forall A (B:A->Type), DependentFunctionalRelReification_on B).
+
+(** The easy part *)
+
+Theorem dep_non_dep_functional_rel_reification : 
+  DependentFunctionalRelReification -> FunctionalRelReification.
+Proof.
+intros DepFunReify A B R H.
+  destruct (DepFunReify A (fun _ => B) R H) as (f,Hf).
+  exists f; trivial.
+Qed.
+
+(** Deriving choice on product types requires some computation on
+    singleton propositional types, so we need computational
+    conjunction projections and dependent elimination of conjunction
+    and equality *)
+
+Theorem non_dep_dep_functional_rel_reification : 
+  FunctionalRelReification -> DependentFunctionalRelReification.
+Proof.
+intros AC_fun A B R H.
+pose (B' := { x:A & B x }). 
+pose (R' := fun (x:A) (y:B') => projT1 y = x /\ R (projT1 y) (projT2 y)). 
+destruct (AC_fun A B' R') as (f,Hf).
+intros x. destruct (H x) as (y,(Hy,Huni)).
+  exists (existT (fun x => B x) x y). repeat split; trivial.
+  intros (x',y') (Heqx',Hy').
+  simpl in *.
+  destruct Heqx'.
+  rewrite (Huni y'); trivial.
+exists (fun x => eq_rect _ _ (projT2 (f x)) _ (proj1_inf (Hf x))).
+intro x; destruct (Hf x) as (Heq,HR) using and_indd.
+destruct (f x); simpl in *.
+destruct Heq using eq_indd; trivial.
+Qed.
+
+(**********************************************************************)
+(** *** F. Non contradiction of constructive descriptions wrt functional axioms of choice *)
+
+(** **** F. 1. Non contradiction of indefinite description *)
+
+Lemma relative_non_contradiction_of_indefinite_desc :
+      (ConstructiveIndefiniteDescription -> False)
+   -> (FunctionalChoice -> False).
+Proof.
+intros H AC_fun.
+assert (AC_depfun := non_dep_dep_functional_choice AC_fun).
+pose (A0 := { A:Type & { P:A->Prop & exists x, P x }}).
+pose (B0 := fun x:A0 => projT1 x).
+pose (R0 := fun x:A0 => fun y:B0 x => projT1 (projT2 x) y).
+pose (H0 := fun x:A0 => projT2 (projT2 x)).
+destruct (AC_depfun A0 B0 R0 H0) as (f, Hf).
+apply H.
+intros A P H'.
+exists (f (existT (fun _ => sigT _) A
+            (existT (fun P => exists x, P x) P H'))).
+pose (Hf' := 
+          Hf (existT (fun _ => sigT _) A
+            (existT (fun P => exists x, P x) P H'))).
 assumption.
 Qed.
+
+Lemma constructive_indefinite_descr_fun_choice :
+   ConstructiveIndefiniteDescription -> FunctionalChoice.
+Proof.
+intros IndefDescr A B R H.
+exists (fun x => proj1_sig (IndefDescr B (R x) (H x))).
+intro x.
+apply (proj2_sig (IndefDescr B (R x) (H x))).
+Qed.
+
+(** **** F. 2. Non contradiction of definite description *)
+
+Lemma relative_non_contradiction_of_definite_descr :
+      (ConstructiveDefiniteDescription -> False)
+   -> (FunctionalRelReification -> False).
+Proof.
+intros H FunReify.
+assert (DepFunReify := non_dep_dep_functional_rel_reification FunReify).
+pose (A0 := { A:Type & { P:A->Prop & exists! x, P x }}).
+pose (B0 := fun x:A0 => projT1 x).
+pose (R0 := fun x:A0 => fun y:B0 x => projT1 (projT2 x) y).
+pose (H0 := fun x:A0 => projT2 (projT2 x)).
+destruct (DepFunReify A0 B0 R0 H0) as (f, Hf).
+apply H.
+intros A P H'.
+exists (f (existT (fun _ => sigT _) A
+            (existT (fun P => exists! x, P x) P H'))).
+pose (Hf' := 
+          Hf (existT (fun _ => sigT _) A
+            (existT (fun P => exists! x, P x) P H'))).
+assumption.
+Qed.
+
+Lemma constructive_definite_descr_fun_reification :
+   ConstructiveDefiniteDescription -> FunctionalRelReification.
+Proof.
+intros DefDescr A B R H.
+exists (fun x => proj1_sig (DefDescr B (R x) (H x))).
+intro x.
+apply (proj2_sig (DefDescr B (R x) (H x))).
+Qed.
+
+(**********************************************************************)
+(** *** G. Excluded-middle + definite description => computational excluded-middle *)
+
+(** The idea for the following proof comes from [ChicliPottierSimpson02] *)
+
+(** Classical logic and axiom of unique choice (i.e. functional
+    relation reification), as shown in [ChicliPottierSimpson02],
+    implies the double-negation of excluded-middle in [Set] (which is
+    incompatible with the impredicativity of [Set]).
+
+    We adapt the proof to show that constructive definite description
+    transports excluded-middle from [Prop] to [Set].
+
+    [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos
+    Simpson, Mathematical Quotients and Quotient Types in Coq,
+    Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646,
+    Springer Verlag.  *)
+
+Require Import Setoid.
+
+Theorem constructive_definite_descr_excluded_middle :
+  ConstructiveDefiniteDescription ->
+  (forall P:Prop, P \/ ~ P) -> (forall P:Prop, {P} + {~ P}).
+Proof.
+intros Descr EM P.
+pose (select := fun b:bool => if b then P else ~P).
+assert { b:bool | select b } as ([|],HP).
+  apply Descr.
+  rewrite <- unique_existence; split.
+  destruct (EM P).
+      exists true; trivial.
+      exists false; trivial.
+    intros [|] [|] H1 H2; simpl in *; reflexivity || contradiction.
+left; trivial.
+right; trivial.
+Qed.  
diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v
index 5b347b1be..51f1b3eff 100644
--- a/theories/Logic/ClassicalChoice.v
+++ b/theories/Logic/ClassicalChoice.v
@@ -8,26 +8,38 @@
 
 (*i $Id$ i*)
 
-(** This file provides classical logic and functional choice *)
+(** This file provides classical logic, and functional choice *)
 
-(** This file extends ClassicalDescription.v with the axiom of choice.
-    As ClassicalDescription.v, it implies the double-negation of
-    excluded-middle in Set and implies a strongly classical
-    world. Especially it conflicts with impredicativity of Set, knowing
-    that [true<>false] in Set.
-*)
+(** This file extends ClassicalUniqueChoice.v with the axiom of choice.
+    As ClassicalUniqueChoice.v, it implies the double-negation of
+    excluded-middle in [Set] and leads to a classical world populated
+    with non computable functions. Especially it conflicts with the
+    impredicativity of [Set], knowing that [true<>false] in [Set].  *)
 
-Require Export ClassicalDescription.
+Require Export ClassicalUniqueChoice.
 Require Export RelationalChoice.
 Require Import ChoiceFacts.
 
+Set Implicit Arguments.
+
+Definition subset (U:Type) (P Q:U->Prop) : Prop := forall x, P x -> Q x.
+
+Theorem singleton_choice :
+  forall (A : Type) (P : A->Prop),
+  (exists x : A, P x) -> exists P' : A->Prop, subset P' P /\ exists! x, P' x.
+Proof.
+intros A P H.
+destruct (relational_choice unit A (fun _ => P) (fun _ => H)) as (R',(Hsub,HR')).
+exists (R' tt); firstorder.
+Qed.
+
 Theorem choice :
- forall (A B:Type) (R:A -> B -> Prop),
-   (forall x:A, exists y : B, R x y) ->
-    exists f : A -> B, (forall x:A, R x (f x)).
+ forall (A B : Type) (R : A->B->Prop),
+   (forall x : A, exists y : B, R x y) ->
+    exists f : A->B, (forall x : A, R x (f x)).
 Proof.
 intros A B.
 apply description_rel_choice_imp_funct_choice.
-exact (description A B).
+exact (unique_choice A B).
 exact (relational_choice A B).
 Qed.
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index 2f175981f..2e15732ef 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -10,69 +10,91 @@
 
 (** This file provides classical logic and definite description *)
 
-(** Classical logic and definite description, as shown in [1],
-    implies the double-negation of excluded-middle in Set, hence it
-    implies a strongly classical world. Especially it conflicts with
-    impredicativity of Set, knowing that true<>false in Set.
+(** Classical definite description operator (i.e. iota) implies
+    excluded-middle in [Set] and leads to a classical world populated
+    with non computable functions. It conflicts with the
+    impredicativity of [Set] *)
 
-    [1] Laurent Chicli, Loïc Pottier, Carlos Simpson, Mathematical
-    Quotients and Quotient Types in Coq, Proceedings of TYPES 2002,
-    Lecture Notes in Computer Science 2646, Springer Verlag.
-*)
+Set Implicit Arguments.
 
 Require Export Classical.
+Require Import ChoiceFacts.
 
-Axiom
-  dependent_description :
-    forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
-      (forall x:A,
-          exists y : B x, R x y /\ (forall y':B x, R x y' -> y = y')) ->
-       exists f : forall x:A, B x, (forall x:A, R x (f x)).
+Notation Local "'inhabited' A" := A (at level 200, only parsing).
+
+Axiom constructive_definite_description :
+  forall (A : Type) (P : A->Prop), (exists! x : A, P x) -> { x : A | P x }.
+
+(** The idea for the following proof comes from [ChicliPottierSimpson02] *)
+
+Theorem excluded_middle_informative : forall P:Prop, {P} + {~ P}.
+Proof.
+apply 
+  (constructive_definite_descr_excluded_middle 
+   constructive_definite_description classic).
+Qed.
+
+Theorem classical_definite_description : 
+  forall (A : Type) (P : A->Prop), inhabited A ->
+  { x : A | (exists! x : A, P x) -> P x }.
+Proof.
+intros A P i.
+destruct (excluded_middle_informative (exists! x, P x)) as [Hex|HnonP].
+  apply constructive_definite_description with (P:= fun x => (exists! x : A, P x) -> P x).
+  destruct Hex as (x,(Hx,Huni)).
+  exists x; split.
+    intros _; exact Hx.
+    firstorder.
+exists i; tauto.
+Qed.
+
+(** Church's iota operator *)
 
-(** Principle of definite descriptions (aka axiom of unique choice) *)
+Definition iota (A : Type) (i:inhabited A) (P : A->Prop) : A
+  := proj1_sig (classical_definite_description P i).
+
+Definition iota_spec (A : Type) (i:inhabited A) (P : A->Prop) : 
+  (exists! x:A, P x) -> P (iota i P)
+  := proj2_sig (classical_definite_description P i).
+
+(** Weaker lemmas (compatibility lemmas) *)
+
+Unset Implicit Arguments.
+
+Lemma dependent_description :
+    forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
+      (forall x:A, exists! y : B x, R x y) ->
+      (exists f : (forall x:A, B x), forall x:A, R x (f x)).
+Proof.
+intros A B R H.
+assert (Hexuni:forall x, exists! y, R x y).
+  intro x. apply H.
+exists (fun x => proj1_sig (constructive_definite_description (R x) (Hexuni x))).
+intro x.
+apply (proj2_sig (constructive_definite_description (R x) (Hexuni x))).
+Qed.
 
 Theorem description :
  forall (A B:Type) (R:A -> B -> Prop),
-   (forall x:A,  exists y : B, R x y /\ (forall y':B, R x y' -> y = y')) ->
-    exists f : A -> B, (forall x:A, R x (f x)).
+   (forall x : A,  exists! y : B, R x y) ->
+   (exists f : A->B, forall x:A, R x (f x)).
 Proof.
 intros A B.
 apply (dependent_description A (fun _ => B)).
 Qed.
 
-(** The followig proof comes from [1] *)
+(** Axiom of unique "choice" (functional reification of functional relations) *)
+
+Set Implicit Arguments.
 
-Theorem classic_set : ((forall P:Prop, {P} + {~ P}) -> False) -> False.
+Require Import Setoid.
+
+Theorem unique_choice :
+ forall (A B:Type) (R:A -> B -> Prop),
+   (forall x:A,  exists! y : B, R x y) ->
+   (exists f : A -> B, forall x:A, R x (f x)).
 Proof.
-intro HnotEM.
-set (R := fun A b => A /\ true = b \/ ~ A /\ false = b).
-assert (H :  exists f : Prop -> bool, (forall A:Prop, R A (f A))).
-apply description.
-intro A.
-destruct (classic A) as [Ha| Hnota].
-  exists true; split.
-    left; split; [ assumption | reflexivity ].
-    intros y [[_ Hy]| [Hna _]].
-      assumption.
-      contradiction.
-  exists false; split.
-    right; split; [ assumption | reflexivity ].
-    intros y [[Ha _]| [_ Hy]].
-      contradiction.
-      assumption.
-destruct H as [f Hf].
-apply HnotEM.
-intro P.
-assert (HfP := Hf P).
-(* Elimination from Hf to Set is not allowed but from f to Set yes ! *)
-destruct (f P).
-  left.
-  destruct HfP as [[Ha _]| [_ Hfalse]].
-    assumption.
-    discriminate.
-  right.
-  destruct HfP as [[_ Hfalse]| [Hna _]].
-    discriminate.
-    assumption.
+intros A B R H.
+apply (description A B).
+intro x. apply H.
 Qed.
- 
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index 7edd66708..e3307d53f 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v
index d714b3bf7..8d2e946de 100644
--- a/theories/Logic/Classical_Prop.v
+++ b/theories/Logic/Classical_Prop.v
@@ -22,6 +22,15 @@ unfold not in |- *; intros; elim (classic p); auto.
 intro NP; elim (H NP).
 Qed.
 
+(** Peirce's law states [forall P Q:Prop, ((P -> Q) -> P) -> P]. 
+    Thanks to [forall P, False -> P], it is equivalent to the
+    following form *)
+
+Lemma Peirce : forall P:Prop, ((P -> False) -> P) -> P.
+Proof.
+intros P H; destruct (classic P); auto.
+Qed.
+
 Lemma not_imply_elim : forall P Q:Prop, ~ (P -> Q) -> P.
 Proof.
 intros; apply NNPP; red in |- *.
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index 5f7112fd7..6b825d47a 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -8,24 +9,44 @@
 
 (*i $Id$ i*)
 
-(** 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.
+(** Diaconescu showed that the Axiom of Choice entails Excluded-Middle
+   in topoi [Diaconescu75]. Lacas and Werner adapted the proof to show
+   that the axiom of choice in equivalence classes entails
+   Excluded-Middle in Type Theory [LacasWerner99].
 
-   This is an adaptatation of the proof by Hugo Herbelin to show that
-   the relational form of the Axiom of Choice + Extensionality for
-   predicates entails Excluded-Middle
+   Three variants of Diaconescu's result in type theory are shown below.
 
-   [Diaconescu] R. Diaconescu, Axiom of Choice and Complementation, in
-   Proceedings of AMS, vol 51, pp 176-178, 1975.
+   A. A proof that the relational form of the Axiom of Choice +
+      Extensionality for Predicates entails Excluded-Middle (by Hugo
+      Herbelin)
 
-   [LacasWerner] S. Lacas, B Werner, Which Choices imply the excluded middle?,
-   preprint, 1999.
+   B. A proof that the relational form of the Axiom of Choice + Proof
+      Irrelevance entails Excluded-Middle for Equality Statements (by
+      Benjamin Werner)
 
+   C. A proof that extensional Hilbert epsilon's description operator
+      entails excluded-middle (taken from Bell [Bell93])
+
+   See also [Carlström] for a discussion of the connection between the
+   Extensional Axiom of Choice and Excluded-Middle
+
+   [Diaconescu75] Radu Diaconescu, Axiom of Choice and Complementation,
+   in Proceedings of AMS, vol 51, pp 176-178, 1975.
+
+   [LacasWerner99] Samuel Lacas, Benjamin Werner, Which Choices imply
+   the excluded middle?, preprint, 1999.
+
+   [Bell93] John L. Bell, Hilbert's epsilon operator and classical
+   logic, Journal of Philosophical Logic, 22: 1-18, 1993
+
+   [Carlström04] Jesper Carlström, EM + Ext_ + AC_int <-> AC_ext,
+   Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004.
 *)
 
-Section PredExt_GuardRelChoice_imp_EM.
+(**********************************************************************)
+(** *** A. Pred. Ext. + Rel. Axiom of Choice -> Excluded-Middle       *)
+
+Section PredExt_RelChoice_imp_EM.
 
 (** The axiom of extensionality for predicates *)
 
@@ -59,15 +80,9 @@ Qed.
 
 Require Import ChoiceFacts.
 
-Variable rel_choice : forall A B:Type, RelationalChoice A B.
+Variable rel_choice : RelationalChoice.
 
-Lemma guarded_rel_choice :
- forall (A B:Type) (P:A -> Prop) (R:A -> B -> Prop),
-   (forall x:A, P x ->  exists y : B, R x y) ->
-     exists R' : A -> B -> Prop,
-     (forall x:A,
-        P x ->
-         exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
+Lemma guarded_rel_choice : GuardedRelationalChoice.
 Proof.
  apply
   (rel_choice_and_proof_irrel_imp_guarded_rel_choice rel_choice proof_irrel).
@@ -78,16 +93,19 @@ Qed.
 
 Require Import Bool.
 
-Lemma AC :
+Lemma AC_bool_subset_to_bool :
   exists R : (bool -> Prop) -> bool -> Prop,
    (forall P:bool -> Prop,
       (exists b : bool, P b) ->
        exists b : bool, P b /\ R P b /\ (forall b':bool, R P b' -> b = b')).
 Proof.
-  apply guarded_rel_choice with
-   (P := fun Q:bool -> Prop =>  exists y : _, Q y)
-   (R := fun (Q:bool -> Prop) (y:bool) => Q y).
-  exact (fun _ H => H).
+  destruct (guarded_rel_choice _ _ 
+   (fun Q:bool -> Prop =>  exists y : _, Q y)
+   (fun (Q:bool -> Prop) (y:bool) => Q y)) as (R,(HRsub,HR)).
+    exact (fun _ H => H).
+  exists R; intros P HP. 
+  destruct (HR P HP) as (y,(Hy,Huni)).
+  exists y; firstorder.
 Qed.
 
 (** The proof of the excluded middle *)
@@ -98,7 +116,7 @@ Proof.
 intro P.
 
 (** first we exhibit the choice functional relation R *)
-destruct AC as [R H].
+destruct AC_bool_subset_to_bool as [R H].
 
 set (class_of_true := fun b => b = true \/ P).
 set (class_of_false := fun b => b = false \/ P).
@@ -135,4 +153,152 @@ left; assumption.
 
 Qed.
 
-End PredExt_GuardRelChoice_imp_EM.
+End PredExt_RelChoice_imp_EM.
+
+(**********************************************************************)
+(** *** B. Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality *)
+
+(** This is an adaptation of Diaconescu's paradox exploiting that
+    proof-irrelevance is some form of extensionality *)
+
+Section ProofIrrel_RelChoice_imp_EqEM.
+
+Variable rel_choice : RelationalChoice.
+
+Variable proof_irrelevance : forall P:Prop , forall x y:P, x=y.
+
+(** Let [a1] and [a2] be two elements in some type [A] *)
+
+Variable A :Type.
+Variables a1 a2 : A.
+
+(** We build the subset [A'] of [A] made of [a1] and [a2] *)
+
+Definition A' := sigT (fun x => x=a1 \/ x=a2).
+
+Definition a1':A'.
+exists a1 ; auto.
+Defined.
+
+Definition a2':A'.
+exists a2 ; auto.
+Defined.
+
+(** By proof-irrelevance, projection is a retraction *)
+
+Lemma projT1_injective : a1=a2 -> a1'=a2'.
+Proof.
+  intro Heq ; unfold a1', a2', A'.
+  rewrite Heq.
+  replace (or_introl (a2=a2) (refl_equal a2)) 
+     with (or_intror (a2=a2) (refl_equal a2)).
+  reflexivity.
+  apply proof_irrelevance.
+Qed.
+
+(** But from the actual proofs of being in [A'], we can assert in the
+    proof-irrelevant world the existence of relevant boolean witnesses *)
+
+Lemma decide : forall x:A', exists y:bool ,
+  (projT1 x = a1 /\ y = true ) \/ (projT1 x = a2 /\ y = false).
+Proof.
+  intros [a [Ha1|Ha2]]; [exists true | exists false]; auto.
+Qed.
+
+(** Thanks to the axiom of choice, the boolean witnesses move from the
+    propositional world to the relevant world *)
+
+Theorem proof_irrel_rel_choice_imp_eq_dec : a1=a2 \/ ~a1=a2.
+Proof.
+  destruct 
+    (rel_choice A' bool 
+       (fun x y =>  projT1 x = a1 /\ y = true \/ projT1 x = a2 /\ y = false))
+    as (R,(HRsub,HR)). 
+    apply decide.
+  destruct (HR a1') as (b1,(Ha1'b1,_Huni1)).
+  destruct (HRsub a1' b1 Ha1'b1) as [(_, Hb1true)|(Ha1a2, _Hb1false)].
+  destruct (HR a2') as (b2,(Ha2'b2,Huni2)).
+  destruct (HRsub a2' b2 Ha2'b2) as [(Ha2a1, _Hb2true)|(_, Hb2false)].
+    left; symmetry; assumption.
+    right; intro H.
+    subst b1; subst b2.
+    rewrite (projT1_injective H) in Ha1'b1.
+    assert (false = true) by auto using Huni2.
+    discriminate.
+  left; assumption.
+Qed.
+
+(** An alternative more concise proof can be done by directly using
+    the guarded relational choice *)
+
+Declare Implicit Tactic auto.
+
+Lemma proof_irrel_rel_choice_imp_eq_dec' : a1=a2 \/ ~a1=a2.
+Proof.
+  assert (decide: forall x:A, x=a1 \/ x=a2 -> 
+                exists y:bool, x=a1 /\ y=true \/ x=a2 /\ y=false).
+    intros a [Ha1|Ha2]; [exists true | exists false]; auto.
+  assert (guarded_rel_choice := 
+          rel_choice_and_proof_irrel_imp_guarded_rel_choice 
+	  rel_choice 
+	  proof_irrelevance).
+  destruct 
+    (guarded_rel_choice A bool 
+      (fun x => x=a1 \/ x=a2)
+      (fun x y => x=a1 /\ y=true \/ x=a2 /\ y=false))
+      as (R,(HRsub,HR)). 
+      apply decide.
+  destruct (HR a1) as (b1,(Ha1b1,_Huni1)). left; reflexivity.
+  destruct (HRsub a1 b1 Ha1b1) as [(_, Hb1true)|(Ha1a2, _Hb1false)].
+  destruct (HR a2) as (b2,(Ha2b2,Huni2)). right; reflexivity.
+  destruct (HRsub a2 b2 Ha2b2) as [(Ha2a1, _Hb2true)|(_, Hb2false)].
+    left; symmetry; assumption.
+    right; intro H.
+    subst b1; subst b2; subst a1.
+    assert (false = true) by auto using Huni2, Ha1b1.
+    discriminate.
+  left; assumption.
+Qed.
+
+End ProofIrrel_RelChoice_imp_EqEM.
+
+(**********************************************************************)
+(** *** B. Extensional Hilbert's epsilon description operator -> Excluded-Middle *)
+
+(** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *)
+
+Notation Local "'inhabited' A" := A (at level 10, only parsing).
+
+Section ExtensionalEpsilon_imp_EM.
+
+Variable epsilon : forall A : Type, inhabited A -> (A -> Prop) -> A.
+
+Hypothesis epsilon_spec : 
+  forall (A:Type) (i:inhabited A) (P:A->Prop), 
+  (exists x, P x) -> P (epsilon A i P).
+
+Hypothesis epsilon_extensionality :
+  forall (A:Type) (i:inhabited A) (P Q:A->Prop),
+  (forall a, P a <-> Q a) -> epsilon A i P = epsilon A i Q.
+
+Notation Local eps := (epsilon bool true) (only parsing).
+
+Theorem extensional_epsilon_imp_EM : forall P:Prop, P \/ ~ P.
+Proof.
+intro P.
+pose (B := fun y => y=false \/ P).
+pose (C := fun y => y=true  \/ P).
+assert (B (eps B)) as [Hfalse|HP] 
+  by (apply epsilon_spec; exists false; left; reflexivity).
+assert (C (eps C)) as [Htrue|HP] 
+  by (apply epsilon_spec; exists true; left; reflexivity).
+  right; intro HP.
+  assert (forall y, B y <-> C y) by (intro y; split; intro; right; assumption).
+  rewrite epsilon_extensionality with (1:=H) in Hfalse.
+  rewrite Htrue in Hfalse.
+  discriminate.
+auto.
+auto.
+Qed.
+
+End ExtensionalEpsilon_imp_EM.
diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v
index feb11b827..9ad6b7220 100644
--- a/theories/Logic/RelationalChoice.v
+++ b/theories/Logic/RelationalChoice.v
@@ -10,11 +10,8 @@
 
 (** This file axiomatizes the relational form of the axiom of choice *)
 
-Axiom
-  relational_choice :
-    forall (A B:Type) (R:A -> B -> Prop),
-      (forall x:A,  exists y : B, R x y) ->
-       exists R' : A -> B -> Prop,
-        (forall x:A,
-            exists y : B,
-             R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
+Axiom relational_choice :
+  forall (A B : Type) (R : A->B->Prop),
+   (forall x : A, exists y : B, R x y) ->
+     exists R' : A->B->Prop, 
+       subrelation R' R /\ forall x : A, exists! y : B, R' x y.