7 files changed, 785 insertions, 755 deletions

diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index d2b7db04..3b066cfc 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -7,9 +7,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ChoiceFacts.v 8999 2006-07-04 12:46:04Z notin $ i*)
+(*i $Id: ChoiceFacts.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
-(** ** Some facts and definitions concerning choice and description in
+(** Some facts and definitions concerning choice and description in
        intuitionistic logic.
 
 We investigate the relations between the following choice and
@@ -54,21 +54,21 @@ IPL^2   = 2nd-order functional minimal predicate logic (with ex. quant.)
 
 Table of contents
 
-A. Definitions
+1. Definitions
 
-B. IPL_2^2 |- AC_rel + AC! = AC_fun
+2. 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
+3. 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
+4. 2. IPL^2 |- AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker
 
-D. Derivability of choice for decidable relations with well-ordered codomain
+5. Derivability of choice for decidable relations with well-ordered codomain
 
-E. Equivalence of choices on dependent or non dependent functional types
+6. Equivalence of choices on dependent or non dependent functional types
 
-F. Non contradiction of constructive descriptions wrt functional choices
+7. Non contradiction of constructive descriptions wrt functional choices
 
-G. Definite description transports classical logic to the computational world
+8. Definite description transports classical logic to the computational world
 
 References:
 
@@ -87,7 +87,7 @@ Set Implicit Arguments.
 Notation Local "'inhabited' A" := A (at level 10, only parsing).
 
 (**********************************************************************)
-(** *** A. Definitions *)
+(** * Definitions *)
 
 (** Choice, reification and description schemes *)
 
@@ -99,29 +99,29 @@ Variables P:A->Prop.
 
 Variables R:A->B->Prop.
 
-(** **** Constructive choice and description *)
+(** ** 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).
+    (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)).
+    (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)).
+    (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
@@ -130,7 +130,7 @@ Definition FunctionalRelReification_on :=
 
 Definition ConstructiveIndefiniteDescription_on :=
   forall P:A->Prop,
-  (exists x, P x) -> { x:A | P x }.
+    (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
@@ -139,59 +139,59 @@ Definition ConstructiveIndefiniteDescription_on :=
 
 Definition ConstructiveDefiniteDescription_on :=
   forall P:A->Prop,
-  (exists! x, P x) -> { x:A | P x }.
+    (exists! x, P x) -> { x:A | P x }.
 
-(** **** Weakly classical choice and description *)
+(** ** Weakly classical choice and description *)
 
 (** GAC_rel *)
 
 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).
+    (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)).
+    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)).
+    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.
+    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).
+    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 }.
+    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 }.
+    A -> { x:A | (exists! x, P x) -> P x }.
 
 End ChoiceSchemes.
 
@@ -235,10 +235,10 @@ Definition IndependenceOfGeneralPremises :=
 
 Definition SmallDrinker'sParadox :=
   forall (A:Type) (P:A -> Prop), inhabited A ->
-  exists x, (exists x, P x) -> P x.
+    exists x, (exists x, P x) -> P x.
 
 (**********************************************************************)
-(** *** B. AC_rel + PDP = AC_fun
+(** * 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
@@ -251,25 +251,25 @@ Definition SmallDrinker'sParadox :=
 
 Lemma description_rel_choice_imp_funct_choice :
   forall A B : Type,
-  FunctionalRelReification_on A B -> RelationalChoice_on A B -> FunctionalChoice_on A B.
+    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.
-destruct (H0 x) as (y,(HR'xy,Huniq)).
-rewrite <- (Huniq (f x) (Hf x)).
-apply HR'R; assumption.
+  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.
+  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 : 
   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 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.
@@ -279,77 +279,77 @@ Qed.
 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.
-destruct (H x) as (y,(HRxy,_)).
-exists y; exact HRxy.
-(* 2 *)
-exists f; exact H0.
+  intros A B FunCh R H.
+  destruct (FunCh R) as [f H0].
+  (* 1 *)
+  intro x.
+  destruct (H x) as (y,(HRxy,_)).
+  exists y; exact HRxy.
+  (* 2 *)
+  exists f; exact H0.
 Qed.
 
 Theorem FunChoice_Equiv_RelChoice_and_ParamDefinDescr :
   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).
+  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.
 
 (**********************************************************************)
-(** *** C. Connection between the guarded, non guarded and descriptive choices and *)
+(** * 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 *)
 
 (**********************************************************************)
-(** **** C. 1. AC_rel + PI -> GAC_rel and AC_rel + IGP -> GAC_rel and GAC_rel = OAC_rel *)
+(** ** 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 :
   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',(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''; split.
+  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',(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''; 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.
-      rewrite proof_irrel with (a1 := HPx) (a2 := H'Px); exact HR'xy'.
+  exists y; split. exists HPx; exact HR'xy.
+  intros y' (H'Px,HR'xy').
+    apply Huniq.
+    rewrite proof_irrel with (a1 := HPx) (a2 := H'Px); exact HR'xy'.
 Qed.
 
 Lemma rel_choice_indep_of_general_premises_imp_guarded_rel_choice :
- forall A B, inhabited B -> RelationalChoice_on A B -> 
-  IndependenceOfGeneralPremises -> GuardedRelationalChoice_on A B.
+  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)).
+  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.
+  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.
+  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)).
+  intros A B GAC_rel R H.
+  destruct (GAC_rel (fun _ => True) R) as (R',(HR'R,H0)).
   firstorder.
-exists R'; firstorder.
+  exists R'; firstorder.
 Qed.
 
 (** OAC_rel = GAC_rel *)
@@ -357,43 +357,43 @@ Qed.
 Lemma guarded_iff_omniscient_rel_choice :
   GuardedRelationalChoice <-> OmniscientRelationalChoice.
 Proof.
-split.
+  split.
   intros GAC_rel A B R.
-    apply (GAC_rel A B (fun x => exists y, R x y) R); auto.
+  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.
+  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 = OAC_fun = AC_fun + Drinker *)
 
 (** AC_fun + IGP = GAC_fun *)
  
 Lemma guarded_fun_choice_imp_indep_of_general_premises :
- GuardedFunctionalChoice -> IndependenceOfGeneralPremises.
+  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.
+  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.
+  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.
+  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.
+  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 *)
@@ -403,26 +403,26 @@ Qed.
 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.
+  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.
+  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).
+  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.
@@ -435,16 +435,16 @@ but we give a direct proof *)
 Lemma guarded_iff_omniscient_fun_choice :
   GuardedFunctionalChoice <-> OmniscientFunctionalChoice.
 Proof.
-split.
+  split.
   intros GAC_fun A B R Inh.
-    apply (GAC_fun A B (fun x => exists y, R x y) R); auto.
+  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.
+  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 *)
+(** * 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
@@ -468,10 +468,10 @@ 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 le P.
 Proof.
-intros P Pdec (n0,HPn0).
-assert
-   (forall n, (exists n', n'<n /\ P n' /\ forall n'', P n'' -> n'<=n'')
-              \/(forall n', P n' -> n<=n')).
+  intros P Pdec (n0,HPn0).
+  assert
+    (forall n, (exists n', n'<n /\ P n' /\ forall n'', P n'' -> n'<=n'')
+      \/(forall n', P n' -> n<=n')).
   induction n.
   right.
   intros n' Hn'.
@@ -493,43 +493,43 @@ assert
   destruct H0.
   rewrite Heqn; assumption.
   destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0];
-  repeat split;
-  assumption || intros n' (HPn',Hminn'); apply le_antisym; auto.
+    repeat split;
+      assumption || intros n' (HPn',Hminn'); apply le_antisym; auto.
 Qed.
 
 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)).
+  exists f : A -> B, (forall x:A, R x (f x)).
 
 Lemma classical_denumerable_description_imp_fun_choice : 
   forall A:Type, 
-  FunctionalRelReification_on A nat -> 
-  forall R:A->nat->Prop, 
-    (forall x y, decidable (R x y)) -> FunctionalChoice_on_rel 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).
+  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).
   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,_).
-assumption.
+    exists f.
+    intros x.
+    destruct (Hf x) as (Hfx,_).
+    assumption.
 Qed.
 
 (**********************************************************************)
-(** *** E. Choice on dependent and non dependent function types are equivalent *)
+(** * Choice on dependent and non dependent function types are equivalent *)
 
-(** **** E. 1. Choice on dependent and non dependent function types are equivalent *)
+(** ** 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)).
+    (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).
@@ -539,7 +539,7 @@ Notation DependentFunctionalChoice :=
 Theorem dep_non_dep_functional_choice : 
   DependentFunctionalChoice -> FunctionalChoice.
 Proof.
-intros AC_depfun A B R H.
+  intros AC_depfun A B R H.
   destruct (AC_depfun A (fun _ => B) R H) as (f,Hf).
   exists f; trivial.
 Qed.
@@ -558,24 +558,24 @@ Definition proj1_inf (A B:Prop) (p : A/\B) :=
 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.
+  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 *)
+(** ** 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)).
+    (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).
@@ -585,7 +585,7 @@ Notation DependentFunctionalRelReification :=
 Theorem dep_non_dep_functional_rel_reification : 
   DependentFunctionalRelReification -> FunctionalRelReification.
 Proof.
-intros DepFunReify A B R H.
+  intros DepFunReify A B R H.
   destruct (DepFunReify A (fun _ => B) R H) as (f,Hf).
   exists f; trivial.
 Qed.
@@ -598,91 +598,91 @@ Qed.
 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)).
+  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.
+  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 *)
+(** * Non contradiction of constructive descriptions wrt functional axioms of choice *)
 
-(** **** F. 1. Non contradiction of indefinite description *)
+(** ** Non contradiction of indefinite description *)
 
 Lemma relative_non_contradiction_of_indefinite_desc :
-      (ConstructiveIndefiniteDescription -> False)
-   -> (FunctionalChoice -> False).
+  (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.
+  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.
+  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))).
+  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 *)
+(** ** Non contradiction of definite description *)
 
 Lemma relative_non_contradiction_of_definite_descr :
-      (ConstructiveDefiniteDescription -> False)
-   -> (FunctionalRelReification -> False).
+  (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.
+  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.
+  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))).
+  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 *)
+(** * Excluded-middle + definite description => computational excluded-middle *)
 
 (** The idea for the following proof comes from [ChicliPottierSimpson02] *)
 
@@ -705,15 +705,15 @@ 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).
+  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.
+  exists true; trivial.
+  exists false; trivial.
+  intros [|] [|] H1 H2; simpl in *; reflexivity || contradiction.
+  left; trivial.
+  right; trivial.
 Qed.  
diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v
index b7293bec..6d0a9c77 100644
--- a/theories/Logic/ClassicalEpsilon.v
+++ b/theories/Logic/ClassicalEpsilon.v
@@ -6,9 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ClassicalEpsilon.v 8933 2006-06-09 14:08:38Z herbelin $ i*)
+(*i $Id: ClassicalEpsilon.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
-(** *** This file provides classical logic and indefinite description
+(** This file provides classical logic and indefinite description
     (Hilbert's epsilon operator) *)
 
 (** Classical epsilon's operator (i.e. indefinite description) implies
@@ -21,37 +21,39 @@ Require Import ChoiceFacts.
 
 Set Implicit Arguments.
 
-Notation Local "'inhabited' A" := A (at level 200, only parsing).
-
 Axiom constructive_indefinite_description :
   forall (A : Type) (P : A->Prop), 
-  (ex P) -> { x : A | P x }.
+    (exists x, P x) -> { x : A | P x }.
 
 Lemma constructive_definite_description :
   forall (A : Type) (P : A->Prop), 
-  (exists! x : A, P x) -> { x : A | P x }.
+    (exists! x, P x) -> { x : A | P x }.
 Proof.
-intros; apply constructive_indefinite_description; firstorder.
+  intros; apply constructive_indefinite_description; firstorder.
 Qed.
 
 Theorem excluded_middle_informative : forall P:Prop, {P} + {~ P}.
 Proof.
-apply 
-  (constructive_definite_descr_excluded_middle 
-   constructive_definite_description classic).
+  apply 
+    (constructive_definite_descr_excluded_middle 
+      constructive_definite_description classic).
 Qed.
 
 Theorem classical_indefinite_description : 
   forall (A : Type) (P : A->Prop), inhabited A ->
-  { x : A | ex P -> P x }.
+    { x : A | (exists x, P x) -> P x }.
 Proof.
-intros A P i.
-destruct (excluded_middle_informative (exists x, P x)) as [Hex|HnonP].
-  apply constructive_indefinite_description with (P:= fun x => ex P -> P x).
+  intros A P i.
+  destruct (excluded_middle_informative (exists x, P x)) as [Hex|HnonP].
+  apply constructive_indefinite_description 
+    with (P:= fun x => (exists x, P x) -> P x).
   destruct Hex as (x,Hx).
     exists x; intros _; exact Hx.
-    firstorder.
-Qed.
+  assert {x : A | True} as (a,_).
+    apply constructive_indefinite_description with (P := fun _ : A => True).
+    destruct i as (a); firstorder.
+  firstorder.
+Defined.
 
 (** Hilbert's epsilon operator *)
 
@@ -59,11 +61,9 @@ Definition epsilon (A : Type) (i:inhabited A) (P : A->Prop) : A
   := proj1_sig (classical_indefinite_description P i).
 
 Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) : 
-  (ex P) -> P (epsilon i P)
+  (exists x, P x) -> P (epsilon i P)
   := proj2_sig (classical_indefinite_description P i).
 
-Opaque epsilon.
-
 (** Open question: is classical_indefinite_description constructively
     provable from [relational_choice] and
     [constructive_definite_description] (at least, using the fact that
@@ -72,19 +72,31 @@ Opaque epsilon.
     [classical_indefinite_description] is provable (see
     [relative_non_contradiction_of_indefinite_desc]). *)
 
-(** Remark: we use [ex P] rather than [exists x, P x] (which is [ex
-    (fun x => P x)] to ease unification *)
+(** A proof that if [P] is inhabited, [epsilon a P] does not depend on
+    the actual proof that the domain of [P] is inhabited
+    (proof idea kindly provided by Pierre Castéran) *)
+
+Lemma epsilon_inh_irrelevance : 
+   forall (A:Type) (i j : inhabited A) (P:A->Prop),
+   (exists x, P x) -> epsilon i P = epsilon j P.
+Proof.
+ intros.
+ unfold epsilon, classical_indefinite_description.
+ destruct (excluded_middle_informative (exists x : A, P x)) as [|[]]; trivial.
+Qed.
+
+Opaque epsilon.
 
 (** *** Weaker lemmas (compatibility lemmas) *)
 
 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 R H.
-exists (fun x => proj1_sig (constructive_indefinite_description (H x))).
-intro x.
-apply (proj2_sig (constructive_indefinite_description  (H x))).
+  intros A B R H.
+  exists (fun x => proj1_sig (constructive_indefinite_description _ (H x))).
+  intro x.
+  apply (proj2_sig (constructive_indefinite_description _ (H x))).
 Qed.
 
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index 70da74d3..dd911db6 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -7,39 +7,39 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ClassicalFacts.v 8892 2006-06-04 17:59:53Z herbelin $ i*)
+(*i $Id: ClassicalFacts.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
-(** ** Some facts and definitions about classical logic
+(** Some facts and definitions about classical logic
 
 Table of contents:
 
-A. Propositional degeneracy = excluded-middle + propositional extensionality
+1. Propositional degeneracy = excluded-middle + propositional extensionality
 
-B. Classical logic and proof-irrelevance
+2. Classical logic and proof-irrelevance
 
-B. 1. CC |- prop. ext. + A inhabited -> (A = A->A) -> A has fixpoint
+2.1. CC |- prop. ext. + A inhabited -> (A = A->A) -> A has fixpoint
 
-B. 2. CC |- prop. ext. + dep elim on bool -> proof-irrelevance
+2.2. CC |- prop. ext. + dep elim on bool -> proof-irrelevance
 
-B. 3. CIC |- prop. ext. -> proof-irrelevance
+2.3. CIC |- prop. ext. -> proof-irrelevance
 
-B. 4. CC |- excluded-middle + dep elim on bool -> proof-irrelevance
+2.4. CC |- excluded-middle + dep elim on bool -> proof-irrelevance
 
-B. 5. CIC |- excluded-middle -> proof-irrelevance
+2.5. CIC |- excluded-middle -> proof-irrelevance
 
-C. Weak classical axioms
+3. Weak classical axioms
 
-C. 1. Weak excluded middle
+3.1. Weak excluded middle
 
-C. 2. Gödel-Dummet axiom and right distributivity of implication over
+3.2. Gödel-Dummet axiom and right distributivity of implication over
       disjunction
 
-C. 3. Independence of general premises and drinker's paradox
+3 3. Independence of general premises and drinker's paradox
 
 *)
 
 (************************************************************************)
-(** *** A. Prop degeneracy = excluded-middle + prop extensionality      *)
+(** * Prop degeneracy = excluded-middle + prop extensionality      *)
 (**
  i.e.        [(forall A, A=True \/ A=False)
                          <->
@@ -61,41 +61,41 @@ Definition excluded_middle := forall A:Prop, A \/ ~ A.
 
 Lemma prop_degen_ext : prop_degeneracy -> prop_extensionality.
 Proof.
-intros H A B [Hab Hba].
-destruct (H A); destruct (H B).
-  rewrite H1; exact H0.
-  absurd B.
-    rewrite H1; exact (fun H => H).
-    apply Hab; rewrite H0; exact I.
-  absurd A.
-    rewrite H0; exact (fun H => H).
-    apply Hba; rewrite H1; exact I.
-  rewrite H1; exact H0.
+  intros H A B [Hab Hba].
+  destruct (H A); destruct (H B).
+    rewrite H1; exact H0.
+    absurd B.
+      rewrite H1; exact (fun H => H).
+      apply Hab; rewrite H0; exact I.
+    absurd A.
+      rewrite H0; exact (fun H => H).
+      apply Hba; rewrite H1; exact I.
+    rewrite H1; exact H0.
 Qed.
 
 Lemma prop_degen_em : prop_degeneracy -> excluded_middle.
 Proof.
-intros H A.
-destruct (H A).
-  left; rewrite H0; exact I.
-  right; rewrite H0; exact (fun x => x).
+  intros H A.
+  destruct (H A).
+    left; rewrite H0; exact I.
+    right; rewrite H0; exact (fun x => x).
 Qed.
 
 Lemma prop_ext_em_degen :
- prop_extensionality -> excluded_middle -> prop_degeneracy.
+  prop_extensionality -> excluded_middle -> prop_degeneracy.
 Proof.
-intros Ext EM A.
-destruct (EM A).
-  left; apply (Ext A True); split;
-   [ exact (fun _ => I) | exact (fun _ => H) ].
-  right; apply (Ext A False); split; [ exact H | apply False_ind ].
+  intros Ext EM A.
+  destruct (EM A).
+    left; apply (Ext A True); split;
+     [ exact (fun _ => I) | exact (fun _ => H) ].
+    right; apply (Ext A False); split; [ exact H | apply False_ind ].
 Qed.
 
 (************************************************************************)
-(** *** B. Classical logic and proof-irrelevance *)
+(** * Classical logic and proof-irrelevance *)
 
 (************************************************************************)
-(** **** B. 1. CC |- prop ext + A inhabited -> (A = A->A) -> A has fixpoint *)
+(** ** CC |- prop ext + A inhabited -> (A = A->A) -> A has fixpoint *)
 
 (** We successively show that:
 
@@ -110,41 +110,41 @@ Qed.
 Definition inhabited (A:Prop) := A.
 
 Lemma prop_ext_A_eq_A_imp_A :
- prop_extensionality -> forall A:Prop, inhabited A -> (A -> A) = A.
+  prop_extensionality -> forall A:Prop, inhabited A -> (A -> A) = A.
 Proof.
-intros Ext A a.
-apply (Ext (A -> A) A); split; [ exact (fun _ => a) | exact (fun _ _ => a) ].
+  intros Ext A a.
+  apply (Ext (A -> A) A); split; [ exact (fun _ => a) | exact (fun _ _ => a) ].
 Qed.
 
 Record retract (A B:Prop) : Prop := 
   {f1 : A -> B; f2 : B -> A; f1_o_f2 : forall x:B, f1 (f2 x) = x}.
 
 Lemma prop_ext_retract_A_A_imp_A :
- prop_extensionality -> forall A:Prop, inhabited A -> retract A (A -> A).
+  prop_extensionality -> forall A:Prop, inhabited A -> retract A (A -> A).
 Proof.
-intros Ext A a.
-rewrite (prop_ext_A_eq_A_imp_A Ext A a).
-exists (fun x:A => x) (fun x:A => x).
-reflexivity.
+  intros Ext A a.
+  rewrite (prop_ext_A_eq_A_imp_A Ext A a).
+  exists (fun x:A => x) (fun x:A => x).
+  reflexivity.
 Qed.
 
 Record has_fixpoint (A:Prop) : Prop := 
   {F : (A -> A) -> A; Fix : forall f:A -> A, F f = f (F f)}.
 
 Lemma ext_prop_fixpoint :
- prop_extensionality -> forall A:Prop, inhabited A -> has_fixpoint A.
+  prop_extensionality -> forall A:Prop, inhabited A -> has_fixpoint A.
 Proof.
-intros Ext A a.
-case (prop_ext_retract_A_A_imp_A Ext A a); intros g1 g2 g1_o_g2.
-exists (fun f => (fun x:A => f (g1 x x)) (g2 (fun x => f (g1 x x)))).
-intro f.
-pattern (g1 (g2 (fun x:A => f (g1 x x)))) at 1 in |- *.
-rewrite (g1_o_g2 (fun x:A => f (g1 x x))).
-reflexivity.
+  intros Ext A a.
+  case (prop_ext_retract_A_A_imp_A Ext A a); intros g1 g2 g1_o_g2.
+  exists (fun f => (fun x:A => f (g1 x x)) (g2 (fun x => f (g1 x x)))).
+  intro f.
+  pattern (g1 (g2 (fun x:A => f (g1 x x)))) at 1 in |- *.
+  rewrite (g1_o_g2 (fun x:A => f (g1 x x))).
+  reflexivity.
 Qed.
 
 (************************************************************************)
-(** **** B. 2. CC |- prop_ext /\ dep elim on bool -> proof-irrelevance  *)
+(** ** CC |- prop_ext /\ dep elim on bool -> proof-irrelevance  *)
 
 (** [proof_irrelevance] asserts equality of all proofs of a given formula *)
 Definition proof_irrelevance := forall (A:Prop) (a1 a2:A), a1 = a2.
@@ -161,44 +161,44 @@ Definition proof_irrelevance := forall (A:Prop) (a1 a2:A), a1 = a2.
 
 Section Proof_irrelevance_gen.
 
-Variable bool : Prop.
-Variable true : bool.
-Variable false : bool.
-Hypothesis bool_elim : forall C:Prop, C -> C -> bool -> C.
-Hypothesis
-  bool_elim_redl : forall (C:Prop) (c1 c2:C), c1 = bool_elim C c1 c2 true.
-Hypothesis
-  bool_elim_redr : forall (C:Prop) (c1 c2:C), c2 = bool_elim C c1 c2 false.
-Let bool_dep_induction :=
+  Variable bool : Prop.
+  Variable true : bool.
+  Variable false : bool.
+  Hypothesis bool_elim : forall C:Prop, C -> C -> bool -> C.
+  Hypothesis
+    bool_elim_redl : forall (C:Prop) (c1 c2:C), c1 = bool_elim C c1 c2 true.
+  Hypothesis
+    bool_elim_redr : forall (C:Prop) (c1 c2:C), c2 = bool_elim C c1 c2 false.
+  Let bool_dep_induction :=
   forall P:bool -> Prop, P true -> P false -> forall b:bool, P b.
 
-Lemma aux : prop_extensionality -> bool_dep_induction -> true = false.
-Proof.
-intros Ext Ind.
-case (ext_prop_fixpoint Ext bool true); intros G Gfix.
-set (neg := fun b:bool => bool_elim bool false true b).
-generalize (refl_equal (G neg)).
-pattern (G neg) at 1 in |- *.
-apply Ind with (b := G neg); intro Heq.
-rewrite (bool_elim_redl bool false true).
-change (true = neg true) in |- *; rewrite Heq; apply Gfix.
-rewrite (bool_elim_redr bool false true).
-change (neg false = false) in |- *; rewrite Heq; symmetry  in |- *;
- apply Gfix.
-Qed.
-
-Lemma ext_prop_dep_proof_irrel_gen :
- prop_extensionality -> bool_dep_induction -> proof_irrelevance.
-Proof.
-intros Ext Ind A a1 a2.
-set (f := fun b:bool => bool_elim A a1 a2 b).
-rewrite (bool_elim_redl A a1 a2).
-change (f true = a2) in |- *.
-rewrite (bool_elim_redr A a1 a2).
-change (f true = f false) in |- *.
-rewrite (aux Ext Ind).
-reflexivity.
-Qed.
+  Lemma aux : prop_extensionality -> bool_dep_induction -> true = false.
+  Proof.
+    intros Ext Ind.
+    case (ext_prop_fixpoint Ext bool true); intros G Gfix.
+    set (neg := fun b:bool => bool_elim bool false true b).
+    generalize (refl_equal (G neg)).
+    pattern (G neg) at 1 in |- *.
+    apply Ind with (b := G neg); intro Heq.
+    rewrite (bool_elim_redl bool false true).
+    change (true = neg true) in |- *; rewrite Heq; apply Gfix.
+    rewrite (bool_elim_redr bool false true).
+    change (neg false = false) in |- *; rewrite Heq; symmetry  in |- *;
+      apply Gfix.
+  Qed.
+
+  Lemma ext_prop_dep_proof_irrel_gen :
+    prop_extensionality -> bool_dep_induction -> proof_irrelevance.
+  Proof.
+    intros Ext Ind A a1 a2.
+    set (f := fun b:bool => bool_elim A a1 a2 b).
+    rewrite (bool_elim_redl A a1 a2).
+    change (f true = a2) in |- *.
+    rewrite (bool_elim_redr A a1 a2).
+    change (f true = f false) in |- *.
+    rewrite (aux Ext Ind).
+    reflexivity.
+  Qed.
 
 End Proof_irrelevance_gen.
 
@@ -208,29 +208,30 @@ End Proof_irrelevance_gen.
 *)
 
 Section Proof_irrelevance_Prop_Ext_CC.
-
-Definition BoolP := forall C:Prop, C -> C -> C.
-Definition TrueP : BoolP := fun C c1 c2 => c1.
-Definition FalseP : BoolP := fun C c1 c2 => c2.
-Definition BoolP_elim C c1 c2 (b:BoolP) := b C c1 c2.
-Definition BoolP_elim_redl (C:Prop) (c1 c2:C) :
-  c1 = BoolP_elim C c1 c2 TrueP := refl_equal c1.
-Definition BoolP_elim_redr (C:Prop) (c1 c2:C) :
-  c2 = BoolP_elim C c1 c2 FalseP := refl_equal c2.
-
-Definition BoolP_dep_induction :=
-  forall P:BoolP -> Prop, P TrueP -> P FalseP -> forall b:BoolP, P b.
-
-Lemma ext_prop_dep_proof_irrel_cc :
- prop_extensionality -> BoolP_dep_induction -> proof_irrelevance.
-Proof
-  ext_prop_dep_proof_irrel_gen BoolP TrueP FalseP BoolP_elim BoolP_elim_redl
-    BoolP_elim_redr.
+  
+  Definition BoolP := forall C:Prop, C -> C -> C.
+  Definition TrueP : BoolP := fun C c1 c2 => c1.
+  Definition FalseP : BoolP := fun C c1 c2 => c2.
+  Definition BoolP_elim C c1 c2 (b:BoolP) := b C c1 c2.
+  Definition BoolP_elim_redl (C:Prop) (c1 c2:C) :
+    c1 = BoolP_elim C c1 c2 TrueP := refl_equal c1.
+  Definition BoolP_elim_redr (C:Prop) (c1 c2:C) :
+    c2 = BoolP_elim C c1 c2 FalseP := refl_equal c2.
+  
+  Definition BoolP_dep_induction :=
+    forall P:BoolP -> Prop, P TrueP -> P FalseP -> forall b:BoolP, P b.
+  
+  Lemma ext_prop_dep_proof_irrel_cc :
+    prop_extensionality -> BoolP_dep_induction -> proof_irrelevance.
+  Proof.
+    exact (ext_prop_dep_proof_irrel_gen BoolP TrueP FalseP BoolP_elim BoolP_elim_redl
+      BoolP_elim_redr).
+  Qed.
 
 End Proof_irrelevance_Prop_Ext_CC.
 
 (************************************************************************)
-(** **** B. 3. CIC |- prop. ext. -> proof-irrelevance                   *)
+(** ** CIC |- prop. ext. -> proof-irrelevance                   *)
 
 (** In the Calculus of Inductive Constructions, inductively defined booleans
     enjoy dependent case analysis, hence directly proof-irrelevance from
@@ -238,21 +239,22 @@ End Proof_irrelevance_Prop_Ext_CC.
 *)
 
 Section Proof_irrelevance_CIC.
-
-Inductive boolP : Prop :=
-  | trueP : boolP
-  | falseP : boolP.
-Definition boolP_elim_redl (C:Prop) (c1 c2:C) :
-  c1 = boolP_ind C c1 c2 trueP := refl_equal c1.
-Definition boolP_elim_redr (C:Prop) (c1 c2:C) :
-  c2 = boolP_ind C c1 c2 falseP := refl_equal c2.
-Scheme boolP_indd := Induction for boolP Sort Prop.
-
-Lemma ext_prop_dep_proof_irrel_cic : prop_extensionality -> proof_irrelevance.
-Proof
-  fun pe =>
-    ext_prop_dep_proof_irrel_gen boolP trueP falseP boolP_ind boolP_elim_redl
-      boolP_elim_redr pe boolP_indd.
+  
+  Inductive boolP : Prop :=
+    | trueP : boolP
+    | falseP : boolP.
+  Definition boolP_elim_redl (C:Prop) (c1 c2:C) :
+    c1 = boolP_ind C c1 c2 trueP := refl_equal c1.
+  Definition boolP_elim_redr (C:Prop) (c1 c2:C) :
+    c2 = boolP_ind C c1 c2 falseP := refl_equal c2.
+  Scheme boolP_indd := Induction for boolP Sort Prop.
+  
+  Lemma ext_prop_dep_proof_irrel_cic : prop_extensionality -> proof_irrelevance.
+  Proof.
+    exact (fun pe =>
+      ext_prop_dep_proof_irrel_gen boolP trueP falseP boolP_ind boolP_elim_redl
+      boolP_elim_redr pe boolP_indd).
+  Qed.
 
 End Proof_irrelevance_CIC.
 
@@ -267,12 +269,12 @@ End Proof_irrelevance_CIC.
   cannot be refined.
 
   [[Berardi90]] Stefano Berardi, "Type dependence and constructive
-  mathematics", Ph. D. thesis, Dipartimento Matematica, Università di
+  mathematics", Ph. D. thesis, Dipartimento Matematica, Università di
   Torino, 1990.
 *)
 
 (************************************************************************)
-(** **** B. 4. CC |- excluded-middle + dep elim on bool -> proof-irrelevance *)
+(** ** CC |- excluded-middle + dep elim on bool -> proof-irrelevance *)
 
 (** This is a proof in the pure Calculus of Construction that
     classical logic in [Prop] + dependent elimination of disjunction entails
@@ -293,60 +295,61 @@ End Proof_irrelevance_CIC.
 Require Import Hurkens.
 
 Section Proof_irrelevance_EM_CC.
-
-Variable or : Prop -> Prop -> Prop.
-Variable or_introl : forall A B:Prop, A -> or A B.
-Variable or_intror : forall A B:Prop, B -> or A B.
-Hypothesis or_elim : forall A B C:Prop, (A -> C) -> (B -> C) -> or A B -> C.
-Hypothesis
-  or_elim_redl :
+  
+  Variable or : Prop -> Prop -> Prop.
+  Variable or_introl : forall A B:Prop, A -> or A B.
+  Variable or_intror : forall A B:Prop, B -> or A B.
+  Hypothesis or_elim : forall A B C:Prop, (A -> C) -> (B -> C) -> or A B -> C.
+  Hypothesis
+    or_elim_redl :
     forall (A B C:Prop) (f:A -> C) (g:B -> C) (a:A),
       f a = or_elim A B C f g (or_introl A B a).
-Hypothesis
-  or_elim_redr :
+  Hypothesis
+    or_elim_redr :
     forall (A B C:Prop) (f:A -> C) (g:B -> C) (b:B),
       g b = or_elim A B C f g (or_intror A B b).
-Hypothesis
-  or_dep_elim :
+  Hypothesis
+    or_dep_elim :
     forall (A B:Prop) (P:or A B -> Prop),
       (forall a:A, P (or_introl A B a)) ->
       (forall b:B, P (or_intror A B b)) -> forall b:or A B, P b.
-
-Hypothesis em : forall A:Prop, or A (~ A).
-Variable B : Prop.
-Variables b1 b2 : B.
-
-(** [p2b] and [b2p] form a retract if [~b1=b2] *)
-
-Definition p2b A := or_elim A (~ A) B (fun _ => b1) (fun _ => b2) (em A).
-Definition b2p b := b1 = b.
-
-Lemma p2p1 : forall A:Prop, A -> b2p (p2b A).
-Proof.
-  unfold p2b in |- *; intro A; apply or_dep_elim with (b := em A);
-   unfold b2p in |- *; intros.
-  apply (or_elim_redl A (~ A) B (fun _ => b1) (fun _ => b2)).
-  destruct (b H).
-Qed.
-Lemma p2p2 : b1 <> b2 -> forall A:Prop, b2p (p2b A) -> A.
-Proof.
-  intro not_eq_b1_b2.
-  unfold p2b in |- *; intro A; apply or_dep_elim with (b := em A);
-   unfold b2p in |- *; intros.
-  assumption.
-  destruct not_eq_b1_b2.
-  rewrite <- (or_elim_redr A (~ A) B (fun _ => b1) (fun _ => b2)) in H.
-  assumption.
-Qed.
-
-(** Using excluded-middle a second time, we get proof-irrelevance *)
-
-Theorem proof_irrelevance_cc : b1 = b2.
-Proof.
-  refine (or_elim _ _ _ _ _ (em (b1 = b2))); intro H.
+  
+  Hypothesis em : forall A:Prop, or A (~ A).
+  Variable B : Prop.
+  Variables b1 b2 : B.
+  
+  (** [p2b] and [b2p] form a retract if [~b1=b2] *)
+
+  Definition p2b A := or_elim A (~ A) B (fun _ => b1) (fun _ => b2) (em A).
+  Definition b2p b := b1 = b.
+
+  Lemma p2p1 : forall A:Prop, A -> b2p (p2b A).
+  Proof.
+    unfold p2b in |- *; intro A; apply or_dep_elim with (b := em A);
+      unfold b2p in |- *; intros.
+    apply (or_elim_redl A (~ A) B (fun _ => b1) (fun _ => b2)).
+    destruct (b H).
+  Qed.
+
+  Lemma p2p2 : b1 <> b2 -> forall A:Prop, b2p (p2b A) -> A.
+  Proof.
+    intro not_eq_b1_b2.
+    unfold p2b in |- *; intro A; apply or_dep_elim with (b := em A);
+      unfold b2p in |- *; intros.
+    assumption.
+    destruct not_eq_b1_b2.
+    rewrite <- (or_elim_redr A (~ A) B (fun _ => b1) (fun _ => b2)) in H.
+    assumption.
+  Qed.
+
+  (** Using excluded-middle a second time, we get proof-irrelevance *)
+
+  Theorem proof_irrelevance_cc : b1 = b2.
+  Proof.
+    refine (or_elim _ _ _ _ _ (em (b1 = b2))); intro H.
     trivial.
-  apply (paradox B p2b b2p (p2p2 H) p2p1).
-Qed.
+    apply (paradox B p2b b2p (p2p2 H) p2p1).
+  Qed.
 
 End Proof_irrelevance_EM_CC.
 
@@ -357,7 +360,7 @@ End Proof_irrelevance_EM_CC.
 *)
 
 (************************************************************************)
-(** **** B. 5. CIC |- excluded-middle -> proof-irrelevance               *)
+(** ** CIC |- excluded-middle -> proof-irrelevance               *)
 
 (**
     Since, dependent elimination is derivable in the Calculus of
@@ -367,18 +370,19 @@ End Proof_irrelevance_EM_CC.
 
 Section Proof_irrelevance_CCI.
 
-Hypothesis em : forall A:Prop, A \/ ~ A.
-
-Definition or_elim_redl (A B C:Prop) (f:A -> C) (g:B -> C) 
-  (a:A) : f a = or_ind f g (or_introl B a) := refl_equal (f a).
-Definition or_elim_redr (A B C:Prop) (f:A -> C) (g:B -> C) 
-  (b:B) : g b = or_ind f g (or_intror A b) := refl_equal (g b).
-Scheme or_indd := Induction for or Sort Prop.
-
-Theorem proof_irrelevance_cci : forall (B:Prop) (b1 b2:B), b1 = b2.
-Proof
-  proof_irrelevance_cc or or_introl or_intror or_ind or_elim_redl
-    or_elim_redr or_indd em.
+  Hypothesis em : forall A:Prop, A \/ ~ A.
+  
+  Definition or_elim_redl (A B C:Prop) (f:A -> C) (g:B -> C) 
+    (a:A) : f a = or_ind f g (or_introl B a) := refl_equal (f a).
+  Definition or_elim_redr (A B C:Prop) (f:A -> C) (g:B -> C) 
+    (b:B) : g b = or_ind f g (or_intror A b) := refl_equal (g b).
+  Scheme or_indd := Induction for or Sort Prop.
+  
+  Theorem proof_irrelevance_cci : forall (B:Prop) (b1 b2:B), b1 = b2.
+  Proof.
+    exact (proof_irrelevance_cc or or_introl or_intror or_ind or_elim_redl
+      or_elim_redr or_indd em).
+  Qed.
 
 End Proof_irrelevance_CCI.
 
@@ -388,16 +392,16 @@ End Proof_irrelevance_CCI.
     [em : forall A:Prop, {A}+{~A}] in the Set-impredicative CCI.
 *)
 
-(** *** C. Weak classical axioms *)
+(** * Weak classical axioms *)
 
 (** We show the following increasing in the strength of axioms:
  - weak excluded-middle
- - right distributivity of implication over disjunction and Gödel-Dummet axiom
+ - right distributivity of implication over disjunction and Gödel-Dummet axiom
  - independence of general premises and drinker's paradox
  - excluded-middle
 *)
 
-(** **** C. 1. Weak excluded-middle *)
+(** ** Weak excluded-middle *)
 
 (** The weak classical logic based on [~~A \/ ~A] is referred to with
     name KC in {[ChagrovZakharyaschev97]]
@@ -411,20 +415,20 @@ Definition weak_excluded_middle :=
 
 (** The interest in the equivalent variant
     [weak_generalized_excluded_middle] is that it holds even in logic
-    without a primitive [False] connective (like Gödel-Dummett axiom) *)
+    without a primitive [False] connective (like Gödel-Dummett axiom) *)
 
 Definition weak_generalized_excluded_middle := 
   forall A B:Prop, ((A -> B) -> B) \/ (A -> B).
 
-(** **** C. 2. Gödel-Dummett axiom *)
+(** ** Gödel-Dummett axiom *)
 
-(** [(A->B) \/ (B->A)] is studied in [[Dummett59]] and is based on [[Gödel33]].
+(** [(A->B) \/ (B->A)] is studied in [[Dummett59]] and is based on [[Gödel33]].
 
     [[Dummett59]] Michael A. E. Dummett. "A Propositional Calculus
     with a Denumerable Matrix", In the Journal of Symbolic Logic, Vol
     24 No. 2(1959), pp 97-103.
 
-    [[Gödel33]] Kurt Gödel. "Zum intuitionistischen Aussagenkalkül",
+    [[Gödel33]] Kurt Gödel. "Zum intuitionistischen Aussagenkalkül",
     Ergeb. Math. Koll. 4 (1933), pp. 34-38.
  *)
 
@@ -432,7 +436,7 @@ Definition GodelDummett := forall A B:Prop, (A -> B) \/ (B -> A).
 
 Lemma excluded_middle_Godel_Dummett : excluded_middle -> GodelDummett.
 Proof.
-intros EM A B. destruct (EM B) as [HB|HnotB].
+  intros EM A B. destruct (EM B) as [HB|HnotB].
   left; intros _; exact HB.
   right; intros HB; destruct (HnotB HB).
 Qed.
@@ -446,15 +450,15 @@ Definition RightDistributivityImplicationOverDisjunction :=
 Lemma Godel_Dummett_iff_right_distr_implication_over_disjunction :
   GodelDummett <-> RightDistributivityImplicationOverDisjunction.
 Proof.
-split.
-  intros GD A B C HCAB.
-  destruct (GD B A) as [HBA|HAB]; [left|right]; intro HC; 
-    destruct (HCAB HC) as [HA|HB]; [ | apply HBA | apply HAB | ]; assumption.
-  intros Distr A B.
-  destruct (Distr A B (A\/B)) as [HABA|HABB].
-    intro HAB; exact HAB.
-    right; intro HB; apply HABA; right; assumption.
-    left; intro HA; apply HABB; left; assumption.
+  split.
+    intros GD A B C HCAB.
+    destruct (GD B A) as [HBA|HAB]; [left|right]; intro HC; 
+      destruct (HCAB HC) as [HA|HB]; [ | apply HBA | apply HAB | ]; assumption.
+    intros Distr A B.
+    destruct (Distr A B (A\/B)) as [HABA|HABB].
+      intro HAB; exact HAB.
+      right; intro HB; apply HABA; right; assumption.
+      left; intro HA; apply HABB; left; assumption.
 Qed.
 
 (** [(A->B) \/ (B->A)] is stronger than the weak excluded middle *)
@@ -462,12 +466,12 @@ Qed.
 Lemma Godel_Dummett_weak_excluded_middle : 
   GodelDummett -> weak_excluded_middle.
 Proof.
-intros GD A. destruct (GD (~A) A) as [HnotAA|HAnotA].
-  left; intro HnotA; apply (HnotA (HnotAA HnotA)).
-  right; intro HA; apply (HAnotA HA HA).
+  intros GD A. destruct (GD (~A) A) as [HnotAA|HAnotA].
+    left; intro HnotA; apply (HnotA (HnotAA HnotA)).
+    right; intro HA; apply (HAnotA HA HA).
 Qed.
 
-(** **** C. 3. Independence of general premises and drinker's paradox *)
+(** ** Independence of general premises and drinker's paradox *)
 
 (** Independence of general premises is the unconstrained, non
     constructive, version of the Independence of Premises as
@@ -475,13 +479,13 @@ Qed.
 
     It is a generalization to predicate logic of the right
     distributivity of implication over disjunction (hence of
-    Gödel-Dummett axiom) whose own constructive form (obtained by a
+    Gödel-Dummett axiom) whose own constructive form (obtained by a
     restricting the third formula to be negative) is called
     Kreisel-Putnam principle [[KreiselPutnam57]].
 
     [[KreiselPutnam57]], Georg Kreisel and Hilary Putnam. "Eine
-    Unableitsbarkeitsbeweismethode für den intuitionistischen
-    Aussagenkalkül". Archiv für Mathematische Logik und
+    Unableitsbarkeitsbeweismethode für den intuitionistischen
+    Aussagenkalkül". Archiv für Mathematische Logik und
     Graundlagenforschung, 3:74- 78, 1957.
 
     [[Troelstra73]], Anne Troelstra, editor. Metamathematical
@@ -499,33 +503,33 @@ Lemma
   independence_general_premises_right_distr_implication_over_disjunction :
   IndependenceOfGeneralPremises -> RightDistributivityImplicationOverDisjunction.
 Proof.
-intros IP A B C HCAB.
-destruct (IP bool (fun b => if b then A else B) C true) as ([|],H).
-  intro HC; destruct (HCAB HC); [exists true|exists false]; assumption.
-  left; assumption.
-  right; assumption.
+  intros IP A B C HCAB.
+  destruct (IP bool (fun b => if b then A else B) C true) as ([|],H).
+    intro HC; destruct (HCAB HC); [exists true|exists false]; assumption.
+    left; assumption.
+    right; assumption.
 Qed.
 
 Lemma independence_general_premises_Godel_Dummett :
   IndependenceOfGeneralPremises -> GodelDummett.
 Proof.
-destruct Godel_Dummett_iff_right_distr_implication_over_disjunction.
-auto using independence_general_premises_right_distr_implication_over_disjunction.
+  destruct Godel_Dummett_iff_right_distr_implication_over_disjunction.
+  auto using independence_general_premises_right_distr_implication_over_disjunction.
 Qed.
 
 (** Independence of general premises is equivalent to the drinker's paradox *)
 
 Definition DrinkerParadox :=
   forall (A:Type) (P:A -> Prop), 
-  inhabited A -> exists x, (exists x, P x) -> P x.
+    inhabited A -> exists x, (exists x, P x) -> P x.
 
 Lemma independence_general_premises_drinker : 
   IndependenceOfGeneralPremises <-> DrinkerParadox.
 Proof.
-split.
-  intros IP A P InhA; apply (IP A P (exists x, P x) InhA); intro Hx; exact Hx.
-  intros Drinker A P Q InhA H; destruct (Drinker A P InhA) as (x,Hx).
-    exists x; intro HQ; apply (Hx (H HQ)).
+  split.
+    intros IP A P InhA; apply (IP A P (exists x, P x) InhA); intro Hx; exact Hx.
+    intros Drinker A P Q InhA H; destruct (Drinker A P InhA) as (x,Hx).
+      exists x; intro HQ; apply (Hx (H HQ)).
 Qed.
 
 (** Independence of general premises is weaker than (generalized) 
@@ -537,9 +541,9 @@ Definition generalized_excluded_middle :=
 Lemma excluded_middle_independence_general_premises :
   generalized_excluded_middle -> DrinkerParadox.
 Proof.
-intros GEM A P x0.
-destruct (GEM (exists x, P x) (P x0)) as [(x,Hx)|Hnot].
-  exists x; intro; exact Hx.
-  exists x0; exact Hnot.
+  intros GEM A P x0.
+  destruct (GEM (exists x, P x) (P x0)) as [(x,Hx)|Hnot].
+    exists x; intro; exact Hx.
+    exists x0; exact Hnot.
 Qed.
  
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index 19d5d7ec..5f139f35 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Diaconescu.v 8892 2006-06-04 17:59:53Z herbelin $ i*)
+(*i $Id: Diaconescu.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 (** Diaconescu showed that the Axiom of Choice entails Excluded-Middle
    in topoi [Diaconescu75]. Lacas and Werner adapted the proof to show
@@ -44,7 +44,7 @@
 *)
 
 (**********************************************************************)
-(** *** A. Pred. Ext. + Rel. Axiom of Choice -> Excluded-Middle       *)
+(** * Pred. Ext. + Rel. Axiom of Choice -> Excluded-Middle       *)
 
 Section PredExt_RelChoice_imp_EM.
 
@@ -156,7 +156,7 @@ Qed.
 End PredExt_RelChoice_imp_EM.
 
 (**********************************************************************)
-(** *** B. Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality *)
+(** * 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 *)
@@ -263,7 +263,7 @@ Qed.
 End ProofIrrel_RelChoice_imp_EqEM.
 
 (**********************************************************************)
-(** *** B. Extensional Hilbert's epsilon description operator -> Excluded-Middle *)
+(** * Extensional Hilbert's epsilon description operator -> Excluded-Middle *)
 
 (** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *)
 
@@ -285,20 +285,20 @@ 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.
+  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/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index 7963555a..a257ef55 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: EqdepFacts.v 8674 2006-03-30 06:56:50Z herbelin $ i*)
+(*i $Id: EqdepFacts.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 (** This file defines dependent equality and shows its equivalence with
     equality on dependent pairs (inhabiting sigma-types). It derives
@@ -32,70 +32,70 @@
 
 Table of contents:
 
-A. Definition of dependent equality and equivalence with equality
+1. Definition of dependent equality and equivalence with equality
 
-B. Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K
+2. Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K
 
-C. Definition of the functor that builds properties of dependent
+3. Definition of the functor that builds properties of dependent
    equalities assuming axiom eq_rect_eq
 
 *)
 
 (************************************************************************)
-(** *** A. Definition of dependent equality and equivalence with equality of dependent pairs *)
+(** * Definition of dependent equality and equivalence with equality of dependent pairs *)
 
 Section Dependent_Equality.
+  
+  Variable U : Type.
+  Variable P : U -> Type.
 
-Variable U : Type.
-Variable P : U -> Type.
+  (** Dependent equality *)
 
-(** Dependent equality *)
-
-Inductive eq_dep (p:U) (x:P p) : forall q:U, P q -> Prop :=
+  Inductive eq_dep (p:U) (x:P p) : forall q:U, P q -> Prop :=
     eq_dep_intro : eq_dep p x p x.
-Hint Constructors eq_dep: core v62.
+  Hint Constructors eq_dep: core v62.
 
-Lemma eq_dep_refl : forall (p:U) (x:P p), eq_dep p x p x.
-Proof eq_dep_intro.
+  Lemma eq_dep_refl : forall (p:U) (x:P p), eq_dep p x p x.
+  Proof eq_dep_intro.
 
-Lemma eq_dep_sym :
- forall (p q:U) (x:P p) (y:P q), eq_dep p x q y -> eq_dep q y p x.
-Proof.
-  destruct 1; auto.
-Qed.
-Hint Immediate eq_dep_sym: core v62.
+  Lemma eq_dep_sym :
+    forall (p q:U) (x:P p) (y:P q), eq_dep p x q y -> eq_dep q y p x.
+  Proof.
+    destruct 1; auto.
+  Qed.
+  Hint Immediate eq_dep_sym: core v62.
 
-Lemma eq_dep_trans :
- forall (p q r:U) (x:P p) (y:P q) (z:P r),
-   eq_dep p x q y -> eq_dep q y r z -> eq_dep p x r z.
-Proof.
-  destruct 1; auto.
-Qed.
+  Lemma eq_dep_trans :
+    forall (p q r:U) (x:P p) (y:P q) (z:P r),
+      eq_dep p x q y -> eq_dep q y r z -> eq_dep p x r z.
+  Proof.
+    destruct 1; auto.
+  Qed.
 
-Scheme eq_indd := Induction for eq Sort Prop.
+  Scheme eq_indd := Induction for eq Sort Prop.
 
-(** Equivalent definition of dependent equality expressed as a non
-    dependent inductive type *)
+  (** Equivalent definition of dependent equality expressed as a non
+      dependent inductive type *)
 
-Inductive eq_dep1 (p:U) (x:P p) (q:U) (y:P q) : Prop :=
+  Inductive eq_dep1 (p:U) (x:P p) (q:U) (y:P q) : Prop :=
     eq_dep1_intro : forall h:q = p, x = eq_rect q P y p h -> eq_dep1 p x q y.
 
-Lemma eq_dep1_dep :
- forall (p:U) (x:P p) (q:U) (y:P q), eq_dep1 p x q y -> eq_dep p x q y.
-Proof.
-  destruct 1 as (eq_qp, H).
-  destruct eq_qp using eq_indd.
-  rewrite H.
-  apply eq_dep_intro.
-Qed.
-
-Lemma eq_dep_dep1 :
- forall (p q:U) (x:P p) (y:P q), eq_dep p x q y -> eq_dep1 p x q y.
-Proof.
-  destruct 1.
-  apply eq_dep1_intro with (refl_equal p).
-  simpl in |- *; trivial.
-Qed.
+  Lemma eq_dep1_dep :
+    forall (p:U) (x:P p) (q:U) (y:P q), eq_dep1 p x q y -> eq_dep p x q y.
+  Proof.
+    destruct 1 as (eq_qp, H).
+    destruct eq_qp using eq_indd.
+    rewrite H.
+    apply eq_dep_intro.
+  Qed.
+
+  Lemma eq_dep_dep1 :
+    forall (p q:U) (x:P p) (y:P q), eq_dep p x q y -> eq_dep1 p x q y.
+  Proof.
+    destruct 1.
+    apply eq_dep1_intro with (refl_equal p).
+    simpl in |- *; trivial.
+  Qed.
 
 End Dependent_Equality.
 
@@ -105,8 +105,8 @@ Implicit Arguments eq_dep1 [U P].
 (** Dependent equality is equivalent to equality on dependent pairs *)
 
 Lemma eq_sigS_eq_dep :
- forall (U:Set) (P:U -> Set) (p q:U) (x:P p) (y:P q),
-   existS P p x = existS P q y -> eq_dep p x q y.
+  forall (U:Set) (P:U -> Set) (p q:U) (x:P p) (y:P q),
+    existS P p x = existS P q y -> eq_dep p x q y.
 Proof.
   intros.
   dependent rewrite H.
@@ -114,10 +114,10 @@ Proof.
 Qed.
 
 Lemma equiv_eqex_eqdep :
- forall (U:Set) (P:U -> Set) (p q:U) (x:P p) (y:P q),
+  forall (U:Set) (P:U -> Set) (p q:U) (x:P p) (y:P q),
    existS P p x = existS P q y <-> eq_dep p x q y.
 Proof.
-split. 
+  split. 
   (* -> *)
   apply eq_sigS_eq_dep.
   (* <- *)
@@ -125,8 +125,8 @@ split.
 Qed.
 
 Lemma eq_sigT_eq_dep :
- forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
-   existT P p x = existT P q y -> eq_dep p x q y.
+  forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
+    existT P p x = existT P q y -> eq_dep p x q y.
 Proof.
   intros.
   dependent rewrite H.
@@ -134,8 +134,8 @@ Proof.
 Qed.
 
 Lemma eq_dep_eq_sigT :
- forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
-   eq_dep p x q y -> existT P p x = existT P q y.
+  forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
+    eq_dep p x q y -> existT P p x = existT P q y.
 Proof.
   destruct 1; reflexivity.
 Qed.
@@ -146,90 +146,90 @@ Hint Resolve eq_dep_intro: core v62.
 Hint Immediate eq_dep_sym: core v62.
 
 (************************************************************************)
-(** *** B. Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K          *)
+(** * Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K          *)
 
 Section Equivalences.
-
-Variable U:Type.
-
-(** Invariance by Substitution of Reflexive Equality Proofs *)
-
-Definition Eq_rect_eq := 
-  forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
-
-(** Injectivity of Dependent Equality *)
-
-Definition Eq_dep_eq := 
-  forall (P:U->Type) (p:U) (x y:P p), eq_dep p x p y -> x = y.
-
-(** Uniqueness of Identity Proofs (UIP) *)
-
-Definition UIP_ := 
-  forall (x y:U) (p1 p2:x = y), p1 = p2.
-
-(** Uniqueness of Reflexive Identity Proofs *)
-
-Definition UIP_refl_ := 
-  forall (x:U) (p:x = x), p = refl_equal x.
-
-(** Streicher's axiom K *)
-
-Definition Streicher_K_ :=
-  forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
-
-(** Injectivity of Dependent Equality is a consequence of *)
-(** Invariance by Substitution of Reflexive Equality Proof *)
-
-Lemma eq_rect_eq__eq_dep1_eq :
-  Eq_rect_eq -> forall (P:U->Type) (p:U) (x y:P p), eq_dep1 p x p y -> x = y.
-Proof.
-  intro eq_rect_eq.
-  simple destruct 1; intro.
-  rewrite <- eq_rect_eq; auto.
-Qed.
-
-Lemma eq_rect_eq__eq_dep_eq : Eq_rect_eq -> Eq_dep_eq.
-Proof.
-  intros eq_rect_eq; red; intros.
-  apply (eq_rect_eq__eq_dep1_eq eq_rect_eq); apply eq_dep_dep1; trivial.
-Qed.
-
-(** Uniqueness of Identity Proofs (UIP) is a consequence of *)
-(** Injectivity of Dependent Equality *)
-
-Lemma eq_dep_eq__UIP : Eq_dep_eq -> UIP_.
-Proof.
-  intro eq_dep_eq; red.
-  intros; apply eq_dep_eq with (P := fun y => x = y).
-  elim p2 using eq_indd.
-  elim p1 using eq_indd.
-  apply eq_dep_intro.
-Qed.
-
-(** Uniqueness of Reflexive Identity Proofs is a direct instance of UIP *)
-
-Lemma UIP__UIP_refl : UIP_ -> UIP_refl_.
-Proof.
-  intro UIP; red; intros; apply UIP.
-Qed.
-
-(** Streicher's axiom K is a direct consequence of Uniqueness of
-    Reflexive Identity Proofs *)
-
-Lemma UIP_refl__Streicher_K : UIP_refl_ -> Streicher_K_.
-Proof.
-  intro UIP_refl; red; intros; rewrite UIP_refl; assumption.
-Qed.
-
-(** We finally recover from K the Invariance by Substitution of
-    Reflexive Equality Proofs *)
-
-Lemma Streicher_K__eq_rect_eq : Streicher_K_ -> Eq_rect_eq.
-Proof.
-  intro Streicher_K; red; intros.
-  apply Streicher_K with (p := h).
-  reflexivity.
-Qed.
+  
+  Variable U:Type.
+  
+  (** Invariance by Substitution of Reflexive Equality Proofs *)
+  
+  Definition Eq_rect_eq := 
+    forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
+  
+  (** Injectivity of Dependent Equality *)
+  
+  Definition Eq_dep_eq := 
+    forall (P:U->Type) (p:U) (x y:P p), eq_dep p x p y -> x = y.
+  
+  (** Uniqueness of Identity Proofs (UIP) *)
+  
+  Definition UIP_ := 
+    forall (x y:U) (p1 p2:x = y), p1 = p2.
+  
+  (** Uniqueness of Reflexive Identity Proofs *)
+
+  Definition UIP_refl_ := 
+    forall (x:U) (p:x = x), p = refl_equal x.
+
+  (** Streicher's axiom K *)
+
+  Definition Streicher_K_ :=
+    forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
+
+  (** Injectivity of Dependent Equality is a consequence of *)
+  (** Invariance by Substitution of Reflexive Equality Proof *)
+
+  Lemma eq_rect_eq__eq_dep1_eq :
+    Eq_rect_eq -> forall (P:U->Type) (p:U) (x y:P p), eq_dep1 p x p y -> x = y.
+  Proof.
+    intro eq_rect_eq.
+    simple destruct 1; intro.
+    rewrite <- eq_rect_eq; auto.
+  Qed.
+
+  Lemma eq_rect_eq__eq_dep_eq : Eq_rect_eq -> Eq_dep_eq.
+  Proof.
+    intros eq_rect_eq; red; intros.
+    apply (eq_rect_eq__eq_dep1_eq eq_rect_eq); apply eq_dep_dep1; trivial.
+  Qed.
+
+  (** Uniqueness of Identity Proofs (UIP) is a consequence of *)
+  (** Injectivity of Dependent Equality *)
+
+  Lemma eq_dep_eq__UIP : Eq_dep_eq -> UIP_.
+  Proof.
+    intro eq_dep_eq; red.
+    intros; apply eq_dep_eq with (P := fun y => x = y).
+    elim p2 using eq_indd.
+    elim p1 using eq_indd.
+    apply eq_dep_intro.
+  Qed.
+  
+  (** Uniqueness of Reflexive Identity Proofs is a direct instance of UIP *)
+
+  Lemma UIP__UIP_refl : UIP_ -> UIP_refl_.
+  Proof.
+    intro UIP; red; intros; apply UIP.
+  Qed.
+
+  (** Streicher's axiom K is a direct consequence of Uniqueness of
+      Reflexive Identity Proofs *)
+
+  Lemma UIP_refl__Streicher_K : UIP_refl_ -> Streicher_K_.
+  Proof.
+    intro UIP_refl; red; intros; rewrite UIP_refl; assumption.
+  Qed.
+
+  (** We finally recover from K the Invariance by Substitution of
+      Reflexive Equality Proofs *)
+  
+  Lemma Streicher_K__eq_rect_eq : Streicher_K_ -> Eq_rect_eq.
+  Proof.
+    intro Streicher_K; red; intros.
+    apply Streicher_K with (p := h).
+    reflexivity.
+  Qed.
 
 (** Remark: It is reasonable to think that [eq_rect_eq] is strictly
     stronger than [eq_rec_eq] (which is [eq_rect_eq] restricted on [Set]):
@@ -246,37 +246,37 @@ Qed.
 End Equivalences.
 
 Section Corollaries.
-
-Variable U:Type.
-Variable V:Set.
-
-(** UIP implies the injectivity of equality on dependent pairs in Type *)
-
-Definition Inj_dep_pairT :=
-  forall (P:U -> Type) (p:U) (x y:P p),
-    existT P p x = existT P p y -> x = y.
-
-Lemma eq_dep_eq__inj_pairT2 : Eq_dep_eq U -> Inj_dep_pairT.
+  
+  Variable U:Type.
+  Variable V:Set.
+  
+  (** UIP implies the injectivity of equality on dependent pairs in Type *)
+
+  Definition Inj_dep_pairT :=
+    forall (P:U -> Type) (p:U) (x y:P p),
+      existT P p x = existT P p y -> x = y.
+  
+  Lemma eq_dep_eq__inj_pairT2 : Eq_dep_eq U -> Inj_dep_pairT.
+  Proof.
+    intro eq_dep_eq; red; intros.
+    apply eq_dep_eq.
+    apply eq_sigT_eq_dep.
+    assumption.
+ Qed.
+ 
+  (** UIP implies the injectivity of equality on dependent pairs in Set *)
+ 
+ Definition Inj_dep_pairS :=
+   forall (P:V -> Set) (p:V) (x y:P p), existS P p x = existS P p y -> x = y.
+ 
+ Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq V -> Inj_dep_pairS.
  Proof.
    intro eq_dep_eq; red; intros.
    apply eq_dep_eq.
-   apply eq_sigT_eq_dep.
+   apply eq_sigS_eq_dep.
    assumption.
  Qed.
 
-(** UIP implies the injectivity of equality on dependent pairs in Set *)
-
-Definition Inj_dep_pairS :=
-  forall (P:V -> Set) (p:V) (x y:P p), existS P p x = existS P p y -> x = y.
-
-Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq V -> Inj_dep_pairS.
-Proof.
-  intro eq_dep_eq; red; intros.
-  apply eq_dep_eq.
-  apply eq_sigS_eq_dep.
-  assumption.
-Qed.
-
 End Corollaries.
 
 (************************************************************************)
@@ -286,16 +286,16 @@ Module Type EqdepElimination.
 
   Axiom eq_rect_eq :
     forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p),
-    x = eq_rect p Q x p h.
+      x = eq_rect p Q x p h.
 
 End EqdepElimination.
 
 Module EqdepTheory (M:EqdepElimination).
-
-Section Axioms.
-
-Variable U:Type.
-
+  
+  Section Axioms.
+    
+    Variable U:Type.
+    
 (** Invariance by Substitution of Reflexive Equality Proofs *)
 
 Lemma eq_rect_eq :
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 7d71a1a6..740fcfcf 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Eqdep_dec.v 8136 2006-03-05 21:57:47Z herbelin $ i*)
+(*i $Id: Eqdep_dec.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 (** We prove that there is only one proof of [x=x], i.e [refl_equal x].
     This holds if the equality upon the set of [x] is decidable.
@@ -20,149 +20,153 @@
 
 Table of contents:
 
-A. Streicher's K and injectivity of dependent pair hold on decidable types
+1. Streicher's K and injectivity of dependent pair hold on decidable types
 
-B.1. Definition of the functor that builds properties of dependent equalities
+1.1. Definition of the functor that builds properties of dependent equalities
      from a proof of decidability of equality for a set in Type
 
-B.2. Definition of the functor that builds properties of dependent equalities
+1.2. Definition of the functor that builds properties of dependent equalities
      from a proof of decidability of equality for a set in Set
 
 *)
 
 (************************************************************************)
-(** *** A. Streicher's K and injectivity of dependent pair hold on decidable types *)
+(** * Streicher's K and injectivity of dependent pair hold on decidable types *)
 
 Set Implicit Arguments.
 
 Section EqdepDec.
 
   Variable A : Type.
-
+  
   Let comp (x y y':A) (eq1:x = y) (eq2:x = y') : y = y' :=
     eq_ind _ (fun a => a = y') eq2 _ eq1.
 
   Remark trans_sym_eq : forall (x y:A) (u:x = y), comp u u = refl_equal y.
-intros.
-case u; trivial.
-Qed.
-
-
+  Proof.
+    intros.
+    case u; trivial.
+  Qed.
 
   Variable eq_dec : forall x y:A, x = y \/ x <> y.
-
+  
   Variable x : A.
 
-
   Let nu (y:A) (u:x = y) : x = y :=
     match eq_dec x y with
-    | or_introl eqxy => eqxy
-    | or_intror neqxy => False_ind _ (neqxy u)
+      | or_introl eqxy => eqxy
+      | or_intror neqxy => False_ind _ (neqxy u)
     end.
 
   Let nu_constant : forall (y:A) (u v:x = y), nu u = nu v.
-intros.
-unfold nu in |- *.
-case (eq_dec x y); intros.
-reflexivity.
-
-case n; trivial.
-Qed.
+    intros.
+    unfold nu in |- *.
+    case (eq_dec x y); intros.
+    reflexivity.
+  
+    case n; trivial.
+  Qed.
 
 
   Let nu_inv (y:A) (v:x = y) : x = y := comp (nu (refl_equal x)) v.
-
+  
 
   Remark nu_left_inv : forall (y:A) (u:x = y), nu_inv (nu u) = u.
-intros.
-case u; unfold nu_inv in |- *.
-apply trans_sym_eq.
-Qed.
+  Proof.
+    intros.
+    case u; unfold nu_inv in |- *.
+    apply trans_sym_eq.
+  Qed.
 
 
   Theorem eq_proofs_unicity : forall (y:A) (p1 p2:x = y), p1 = p2.
-intros.
-elim nu_left_inv with (u := p1).
-elim nu_left_inv with (u := p2).
-elim nu_constant with y p1 p2.
-reflexivity.
-Qed.
+  Proof.
+    intros.
+    elim nu_left_inv with (u := p1).
+    elim nu_left_inv with (u := p2).
+    elim nu_constant with y p1 p2.
+    reflexivity.
+  Qed.
 
-  Theorem K_dec :
-   forall P:x = x -> Prop, P (refl_equal x) -> forall p:x = x, P p.
-intros.
-elim eq_proofs_unicity with x (refl_equal x) p.
-trivial.
-Qed.
+  Theorem K_dec : 
+    forall P:x = x -> Prop, P (refl_equal x) -> forall p:x = x, P p.
+  Proof.
+    intros.
+    elim eq_proofs_unicity with x (refl_equal x) p.
+    trivial.
+  Qed.
 
   (** The corollary *)
 
   Let proj (P:A -> Prop) (exP:ex P) (def:P x) : P x :=
     match exP with
-    | ex_intro x' prf =>
+      | ex_intro x' prf =>
         match eq_dec x' x with
-        | or_introl eqprf => eq_ind x' P prf x eqprf
-        | _ => def
+          | or_introl eqprf => eq_ind x' P prf x eqprf
+          | _ => def
         end
     end.
 
 
   Theorem inj_right_pair :
-   forall (P:A -> Prop) (y y':P x),
-     ex_intro P x y = ex_intro P x y' -> y = y'.
-intros.
-cut (proj (ex_intro P x y) y = proj (ex_intro P x y') y).
-simpl in |- *.
-case (eq_dec x x).
-intro e.
-elim e using K_dec; trivial.
-
-intros.
-case n; trivial.
-
-case H.
-reflexivity.
-Qed.
+    forall (P:A -> Prop) (y y':P x),
+      ex_intro P x y = ex_intro P x y' -> y = y'.
+  Proof.
+    intros.
+    cut (proj (ex_intro P x y) y = proj (ex_intro P x y') y).
+    simpl in |- *.
+    case (eq_dec x x).
+    intro e.
+    elim e using K_dec; trivial.
+    
+    intros.
+    case n; trivial.
+    
+    case H.
+    reflexivity.
+  Qed.
 
 End EqdepDec.
 
 Require Import EqdepFacts.
 
-  (** We deduce axiom [K] for (decidable) types *)
-  Theorem K_dec_type :
-   forall A:Type,
-     (forall x y:A, {x = y} + {x <> y}) ->
-     forall (x:A) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
-intros A eq_dec x P H p.
-elim p using K_dec; intros.
-case (eq_dec x0 y); [left|right]; assumption.
-trivial.
+(** We deduce axiom [K] for (decidable) types *)
+Theorem K_dec_type :
+  forall A:Type,
+    (forall x y:A, {x = y} + {x <> y}) ->
+    forall (x:A) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
+Proof.
+  intros A eq_dec x P H p.
+  elim p using K_dec; intros.
+  case (eq_dec x0 y); [left|right]; assumption.
+  trivial.
 Qed.
 
-  Theorem K_dec_set :
-   forall A:Set,
-     (forall x y:A, {x = y} + {x <> y}) ->
-     forall (x:A) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
-  Proof fun A => K_dec_type (A:=A).
-
-  (** We deduce the [eq_rect_eq] axiom for (decidable) types *)
-  Theorem eq_rect_eq_dec :
-    forall A:Type,
-     (forall x y:A, {x = y} + {x <> y}) ->
-     forall (p:A) (Q:A -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
-intros A eq_dec.
-apply (Streicher_K__eq_rect_eq A (K_dec_type eq_dec)).
+Theorem K_dec_set :
+  forall A:Set,
+    (forall x y:A, {x = y} + {x <> y}) ->
+    forall (x:A) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
+Proof fun A => K_dec_type (A:=A).
+
+(** We deduce the [eq_rect_eq] axiom for (decidable) types *)
+Theorem eq_rect_eq_dec :
+  forall A:Type,
+    (forall x y:A, {x = y} + {x <> y}) ->
+    forall (p:A) (Q:A -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
+Proof.
+  intros A eq_dec.
+  apply (Streicher_K__eq_rect_eq A (K_dec_type eq_dec)).
 Qed.
 
 Unset Implicit Arguments.
 
 (************************************************************************)
-(** *** B.1. Definition of the functor that builds properties of dependent equalities on decidable sets in Type *)
+(** ** Definition of the functor that builds properties of dependent equalities on decidable sets in Type *)
 
 (** The signature of decidable sets in [Type] *)
 
 Module Type DecidableType.
-
+  
   Parameter U:Type.
   Axiom eq_dec : forall x y:U, {x = y} + {x <> y}.
 
@@ -215,16 +219,17 @@ Module DecidableEqDep (M:DecidableType).
   Lemma inj_pairP2 :
     forall (P:U -> Prop) (x:U) (p q:P x),
       ex_intro P x p = ex_intro P x q -> p = q.
-  intros.
-  apply inj_right_pair with (A:=U).
-  intros x0 y0; case (eq_dec x0 y0); [left|right]; assumption.
-  assumption.
+  Proof.
+    intros.
+    apply inj_right_pair with (A:=U).
+    intros x0 y0; case (eq_dec x0 y0); [left|right]; assumption.
+    assumption.
   Qed.
 
 End DecidableEqDep.
 
 (************************************************************************)
-(** *** B.2 Definition of the functor that builds properties of dependent equalities on decidable sets in Set *)
+(** ** B Definition of the functor that builds properties of dependent equalities on decidable sets in Set *)
 
 (** The signature of decidable sets in [Set] *)
 
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 4d365e32..6a723e43 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: JMeq.v 6009 2004-08-03 17:42:55Z herbelin $ i*)
+(*i $Id: JMeq.v 9077 2006-08-24 08:44:32Z herbelin $ i*)
 
 (** John Major's Equality as proposed by Conor McBride
 
@@ -19,56 +19,65 @@
 
 Set Implicit Arguments.
 
-Inductive JMeq (A:Set) (x:A) : forall B:Set, B -> Prop :=
+Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop :=
     JMeq_refl : JMeq x x.
-Reset JMeq_ind.
+Reset JMeq_rect.
 
 Hint Resolve JMeq_refl.
 
-Lemma sym_JMeq : forall (A B:Set) (x:A) (y:B), JMeq x y -> JMeq y x.
+Lemma sym_JMeq : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x.
 destruct 1; trivial.
 Qed.
 
 Hint Immediate sym_JMeq.
 
 Lemma trans_JMeq :
- forall (A B C:Set) (x:A) (y:B) (z:C), JMeq x y -> JMeq y z -> JMeq x z.
+ forall (A B C:Type) (x:A) (y:B) (z:C), JMeq x y -> JMeq y z -> JMeq x z.
 destruct 1; trivial.
 Qed.
 
-Axiom JMeq_eq : forall (A:Set) (x y:A), JMeq x y -> x = y.
+Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y.
 
-Lemma JMeq_ind : forall (A:Set) (x y:A) (P:A -> Prop), P x -> JMeq x y -> P y.
+Lemma JMeq_ind : forall (A:Type) (x y:A) (P:A -> Prop), P x -> JMeq x y -> P y.
 intros A x y P H H'; case JMeq_eq with (1 := H'); trivial.
 Qed.
 
-Lemma JMeq_rec : forall (A:Set) (x y:A) (P:A -> Set), P x -> JMeq x y -> P y.
+Lemma JMeq_rec : forall (A:Type) (x y:A) (P:A -> Set), P x -> JMeq x y -> P y.
+intros A x y P H H'; case JMeq_eq with (1 := H'); trivial.
+Qed.
+
+Lemma JMeq_rect : forall (A:Type) (x y:A) (P:A->Type), P x -> JMeq x y -> P y.
 intros A x y P H H'; case JMeq_eq with (1 := H'); trivial.
 Qed.
 
 Lemma JMeq_ind_r :
- forall (A:Set) (x y:A) (P:A -> Prop), P y -> JMeq x y -> P x.
+ forall (A:Type) (x y:A) (P:A -> Prop), P y -> JMeq x y -> P x.
 intros A x y P H H'; case JMeq_eq with (1 := sym_JMeq H'); trivial.
 Qed.
 
 Lemma JMeq_rec_r :
- forall (A:Set) (x y:A) (P:A -> Set), P y -> JMeq x y -> P x.
+ forall (A:Type) (x y:A) (P:A -> Set), P y -> JMeq x y -> P x.
+intros A x y P H H'; case JMeq_eq with (1 := sym_JMeq H'); trivial.
+Qed.
+
+Lemma JMeq_rect_r :
+ forall (A:Type) (x y:A) (P:A -> Type), P y -> JMeq x y -> P x.
 intros A x y P H H'; case JMeq_eq with (1 := sym_JMeq H'); trivial.
 Qed.
 
-(** [JMeq] is equivalent to [(eq_dep Set [X]X)] *)
+(** [JMeq] is equivalent to [(eq_dep Type [X]X)] *)
 
 Require Import Eqdep.
 
 Lemma JMeq_eq_dep :
- forall (A B:Set) (x:A) (y:B), JMeq x y -> eq_dep Set (fun X => X) A x B y.
+ forall (A B:Type) (x:A) (y:B), JMeq x y -> eq_dep Type (fun X => X) A x B y.
 Proof.
 destruct 1.
 apply eq_dep_intro.
 Qed.
 
 Lemma eq_dep_JMeq :
- forall (A B:Set) (x:A) (y:B), eq_dep Set (fun X => X) A x B y -> JMeq x y.
+ forall (A B:Type) (x:A) (y:B), eq_dep Type (fun X => X) A x B y -> JMeq x y.
 Proof.
 destruct 1.
 apply JMeq_refl.