Modularisation des preuves concernant la logique classique, l'indiscernabilité des preuves et l'axiome K

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

9 files changed, 862 insertions, 336 deletions

diff --git a/.depend.coq b/.depend.coq
index c649bba755..ed1f9f64d7 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -70,23 +70,25 @@ theories/Init/Wf.vo: theories/Init/Wf.v theories/Init/Notations.vo theories/Init
 theories/Init/Tactics.vo: theories/Init/Tactics.v theories/Init/Notations.vo theories/Init/Logic.vo
 theories/Init/Prelude.vo: theories/Init/Prelude.v theories/Init/Notations.vo theories/Init/Logic.vo theories/Init/Datatypes.vo theories/Init/Specif.vo theories/Init/Peano.vo theories/Init/Wf.vo theories/Init/Tactics.vo
 theories/Logic/Hurkens.vo: theories/Logic/Hurkens.v
-theories/Logic/ProofIrrelevance.vo: theories/Logic/ProofIrrelevance.v theories/Logic/Hurkens.vo
+theories/Logic/ProofIrrelevance.vo: theories/Logic/ProofIrrelevance.v theories/Logic/ProofIrrelevanceFacts.vo
 theories/Logic/Classical.vo: theories/Logic/Classical.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo
 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/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/ProofIrrelevance.vo
-theories/Logic/ClassicalFacts.vo: theories/Logic/ClassicalFacts.v
+theories/Logic/Classical_Prop.vo: theories/Logic/Classical_Prop.v theories/Logic/ClassicalFacts.vo theories/Logic/EqdepFacts.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/Berardi.vo: theories/Logic/Berardi.v
-theories/Logic/Eqdep_dec.vo: theories/Logic/Eqdep_dec.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/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/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
diff --git a/Makefile b/Makefile
index 4ae18b411f..c7e91cd5ae 100644
--- a/Makefile
+++ b/Makefile
@@ -137,7 +137,7 @@ LIBRARY=\
   library/nameops.cmo library/libnames.cmo library/libobject.cmo \
   library/summary.cmo library/nametab.cmo library/global.cmo library/lib.cmo \
   library/declaremods.cmo library/library.cmo library/states.cmo \
-  library/decl_kinds.cmo library/dischargedhypsmap.cmo library/goptions.cmo 
+  library/decl_kinds.cmo library/dischargedhypsmap.cmo library/goptions.cmo
 
 PRETYPING=\
   pretyping/termops.cmo pretyping/evd.cmo \
@@ -790,7 +790,8 @@ LOGICVO=\
  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/RelationalChoice.vo     theories/Logic/Diaconescu.vo \
+ theories/Logic/EqdepFacts.vo           theories/Logic/ProofIrrelevanceFacts.vo
 
 ARITHVO=\
  theories/Arith/Arith.vo        theories/Arith/Gt.vo          \
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index f7f0b5c982..7edd667087 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -8,22 +8,54 @@
 
 (*i $Id$ i*)
 
-(** ** Some facts and definitions about classical logic *)
+(** ** Some facts and definitions about classical logic
 
-(** [prop_degeneracy] (also referred as propositional completeness) *)
-(*  asserts (up to consistency) that there are only two distinct formulas *)
+Table of contents:
+
+A. Propositional degeneracy = excluded-middle + propositional extensionality
+
+B. Classical logic and proof-irrelevance
+
+B. 1. CC |- prop. ext. + A inhabited -> (A = A->A) -> A has fixpoint
+
+B. 2. CC |- prop. ext. + dep elim on bool -> proof-irrelevance
+
+B. 3. CIC |- prop. ext. -> proof-irrelevance
+
+B. 4. CC |- excluded-middle + dep elim on bool -> proof-irrelevance
+
+B. 5. CIC |- excluded-middle -> proof-irrelevance
+
+C. Weak classical axioms
+
+C. 1. Weak excluded middle
+
+C. 2. Gödel-Dummet axiom and right distributivity of implication over
+      disjunction
+
+C. 3. Independence of general premises and drinker's paradox
+
+*)
+
+(************************************************************************)
+(** *** A. Prop degeneracy = excluded-middle + prop extensionality      *)
+(**
+ i.e.        [(forall A, A=True \/ A=False)
+                         <->
+       (forall A, A\/~A) /\ (forall A B, (A<->B) -> A=B)]
+*)
+
+(** [prop_degeneracy] (also referred to as propositional completeness)
+    asserts (up to consistency) that there are only two distinct formulas *)
 Definition prop_degeneracy := forall A:Prop, A = True \/ A = False.
 
-(** [prop_extensionality] asserts equivalent formulas are equal *)
+(** [prop_extensionality] asserts that equivalent formulas are equal *)
 Definition prop_extensionality := forall A B:Prop, (A <-> B) -> A = B.
 
-(** [excluded_middle] asserts we can reason by case on the truth *)
-(*  or falsity of any formula *)
+(** [excluded_middle] asserts that we can reason by case on the truth
+    or falsity of any formula *)
 Definition excluded_middle := forall A:Prop, A \/ ~ A.
 
-(** [proof_irrelevance] asserts equality of all proofs of a given formula *)
-Definition proof_irrelevance := forall (A:Prop) (a1 a2:A), a1 = a2.
-
 (** We show [prop_degeneracy <-> (prop_extensionality /\ excluded_middle)] *)
 
 Lemma prop_degen_ext : prop_degeneracy -> prop_extensionality.
@@ -58,6 +90,12 @@ destruct (EM A).
   right; apply (Ext A False); split; [ exact H | apply False_ind ].
 Qed.
 
+(************************************************************************)
+(** *** B. Classical logic and proof-irrelevance *)
+
+(************************************************************************)
+(** **** B. 1. CC |- prop ext + A inhabited -> (A = A->A) -> A has fixpoint *)
+
 (** We successively show that:
 
    [prop_extensionality]
@@ -104,13 +142,20 @@ rewrite (g1_o_g2 (fun x:A => f (g1 x x))).
 reflexivity.
 Qed.
 
-(** Assume we have booleans with the property that there is at most 2
+(************************************************************************)
+(** **** B. 2. 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.
+
+(** Assume that we have booleans with the property that there is at most 2
     booleans (which is equivalent to dependent case analysis). Consider
     the fixpoint of the negation function: it is either true or false by
     dependent case analysis, but also the opposite by fixpoint. Hence
     proof-irrelevance.
 
-    We then map bool proof-irrelevance to all propositions.
+    We then map equality of boolean proofs to proof irrelevance in all
+    propositions.
 *)
 
 Section Proof_irrelevance_gen.
@@ -161,7 +206,7 @@ End Proof_irrelevance_gen.
     most 2 elements.
 *)
 
-Section Proof_irrelevance_CC.
+Section Proof_irrelevance_Prop_Ext_CC.
 
 Definition BoolP := forall C:Prop, C -> C -> C.
 Definition TrueP : BoolP := fun C c1 c2 => c1.
@@ -181,7 +226,10 @@ Proof
   ext_prop_dep_proof_irrel_gen BoolP TrueP FalseP BoolP_elim BoolP_elim_redl
     BoolP_elim_redr.
 
-End Proof_irrelevance_CC.
+End Proof_irrelevance_Prop_Ext_CC.
+
+(************************************************************************)
+(** **** B. 3. CIC |- prop. ext. -> proof-irrelevance                   *)
 
 (** In the Calculus of Inductive Constructions, inductively defined booleans
     enjoy dependent case analysis, hence directly proof-irrelevance from
@@ -211,21 +259,146 @@ End Proof_irrelevance_CIC.
   (i.e. propositional extensionality + excluded middle) without
   dependent case analysis ?
 
-  Berardi [Berardi] built a model of CC interpreting inhabited
+  Berardi [[Berardi90]] built a model of CC interpreting inhabited
   types by the set of all untyped lambda-terms. This model satisfies
   propositional degeneracy without satisfying proof-irrelevance (nor
   dependent case analysis). This implies that the previous results
   cannot be refined.
 
-  [Berardi] Stefano Berardi, "Type dependence and constructive mathematics",
-  Ph. D. thesis, Dipartimento Matematica, Università di Torino, 1990.
+  [[Berardi90]] Stefano Berardi, "Type dependence and constructive
+  mathematics", Ph. D. thesis, Dipartimento Matematica, Università di
+  Torino, 1990.
 *)
 
-(** *** Standard facts about weak classical axioms *)
+(************************************************************************)
+(** **** B. 4. 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
+    proof-irrelevance.
+
+    Reference:
+
+    [[Coquand90]] T. Coquand, "Metamathematical Investigations of a
+    Calculus of Constructions", Proceedings of Logic in Computer Science
+    (LICS'90), 1990.
 
-(** **** Weak excluded-middle *)
+    Proof skeleton: classical logic + dependent elimination of
+    disjunction + discrimination of proofs implies the existence of a
+    retract from [Prop] into [bool], hence inconsistency by encoding any
+    paradox of system U- (e.g. Hurkens' paradox).
+*)
+
+Require Import Hurkens.
+
+Section Proof_irrelevance_EM_CC.
 
-(** The weak classical logic based on [~~A \/ ~A] is refered to with
+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 :
+    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 :
+    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.
+    trivial.
+  apply (paradox B p2b b2p (p2p2 H) p2p1).
+Qed.
+
+End Proof_irrelevance_EM_CC.
+
+(** Remark: Hurkens' paradox still holds with a retract from the
+    _negative_ fragment of [Prop] into [bool], hence weak classical
+    logic, i.e. [forall A, ~A\/~~A], is enough for deriving
+    proof-irrelevance.
+*)
+
+(************************************************************************)
+(** **** B. 5. CIC |- excluded-middle -> proof-irrelevance               *)
+
+(**
+    Since, dependent elimination is derivable in the Calculus of
+    Inductive Constructions (CCI), we get proof-irrelevance from classical
+    logic in the CCI.
+*)
+
+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.
+
+End Proof_irrelevance_CCI.
+
+(** Remark: in the Set-impredicative CCI, Hurkens' paradox still holds with
+    [bool] in [Set] and since [~true=false] for [true] and [false]
+    in [bool] from [Set], we get the inconsistency of
+    [em : forall A:Prop, {A}+{~A}] in the Set-impredicative CCI.
+*)
+
+(** *** C. 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
+ - independence of general premises and drinker's paradox
+ - excluded-middle
+*)
+
+(** **** C. 1. Weak excluded-middle *)
+
+(** The weak classical logic based on [~~A \/ ~A] is referred to with
     name KC in {[ChagrovZakharyaschev97]]
 
    [[ChagrovZakharyaschev97]] Alexander Chagrov and Michael
@@ -242,7 +415,7 @@ Definition weak_excluded_middle :=
 Definition weak_generalized_excluded_middle := 
   forall A B:Prop, ((A -> B) -> B) \/ (A -> B).
 
-(** **** Gödel-Dummett axiom *)
+(** **** C. 2. Gödel-Dummett axiom *)
 
 (** [(A->B) \/ (B->A)] is studied in [[Dummett59]] and is based on [[Gödel33]].
 
@@ -293,7 +466,7 @@ intros GD A. destruct (GD (~A) A) as [HnotAA|HAnotA].
   right; intro HA; apply (HAnotA HA HA).
 Qed.
 
-(** **** Independence of general premises and drinker's paradox *)
+(** **** C. 3. Independence of general premises and drinker's paradox *)
 
 (** Independence of general premises is the unconstrained, non
     constructive, version of the Independence of Premises as
@@ -315,8 +488,7 @@ Qed.
     344 of Lecture Notes in Mathematics, Springer-Verlag, 1973.
 *)
 
-
-Notation "'inhabited' A" := A (at level 10, only parsing).
+Notation Local "'inhabited' A" := A (at level 10, only parsing).
 
 Definition IndependenceOfGeneralPremises :=
   forall (A:Type) (P:A -> Prop) (Q:Prop),
@@ -354,3 +526,19 @@ split.
   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) 
+    excluded middle *)
+
+Definition generalized_excluded_middle := 
+  forall A B:Prop, A \/ (A -> B).
+
+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.
+Qed.
+ 
diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v
index 1df6a354bd..d714b3bf7b 100755
--- a/theories/Logic/Classical_Prop.v
+++ b/theories/Logic/Classical_Prop.v
@@ -10,7 +10,7 @@
 
 (** Classical Propositional Logic *)
 
-Require Import ProofIrrelevance.
+Require Import ClassicalFacts.
 
 Hint Unfold not: core.
 
@@ -29,8 +29,8 @@ intro; apply H; intro; absurd P; trivial.
 Qed.
 
 Lemma not_imply_elim2 : forall P Q:Prop, ~ (P -> Q) -> ~ Q.
-Proof.
-intros; elim (classic Q); auto.
+Proof. (* Intuitionistic *)
+tauto.
 Qed.
 
 Lemma imply_to_or : forall P Q:Prop, (P -> Q) -> ~ P \/ Q.
@@ -46,9 +46,8 @@ apply not_imply_elim2 with P; trivial.
 Qed.
 
 Lemma or_to_imply : forall P Q:Prop, ~ P \/ Q -> P -> Q.
-Proof.
-simple induction 1; auto.
-intros H1 H2; elim (H1 H2).
+Proof. (* Intuitionistic *)
+tauto.
 Qed.
 
 Lemma not_and_or : forall P Q:Prop, ~ (P /\ Q) -> ~ P \/ ~ Q.
@@ -62,23 +61,23 @@ simple induction 1; red in |- *; simple induction 2; auto.
 Qed.
 
 Lemma not_or_and : forall P Q:Prop, ~ (P \/ Q) -> ~ P /\ ~ Q.
-Proof.
-intros; elim (classic P); auto.
+Proof. (* Intuitionistic *)
+tauto.
 Qed.
 
 Lemma and_not_or : forall P Q:Prop, ~ P /\ ~ Q -> ~ (P \/ Q).
-Proof.
-simple induction 1; red in |- *; simple induction 3; trivial.
+Proof. (* Intuitionistic *)
+tauto.
 Qed.
 
 Lemma imply_and_or : forall P Q:Prop, (P -> Q) -> P \/ Q -> Q.
-Proof.
-simple induction 2; trivial.
+Proof. (* Intuitionistic *)
+tauto.
 Qed.
 
 Lemma imply_and_or2 : forall P Q R:Prop, (P -> Q) -> P \/ R -> Q \/ R.
-Proof.
-simple induction 2; auto.
+Proof. (* Intuitionistic *)
+tauto.
 Qed.
 
 Lemma proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.
@@ -93,4 +92,19 @@ end.
 
 Ltac classical_left := match goal with 
 | _:_ |- _ \/?X1 => (elim (classic X1);intro;[right;trivial|left])
-end.
\ No newline at end of file
+end.
+
+Require Export EqdepFacts.
+
+Module Eq_rect_eq.
+
+Lemma 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.
+Proof.
+intros; rewrite proof_irrelevance with (p1:=h) (p2:=refl_equal p); reflexivity.
+Qed.
+
+End Eq_rect_eq.
+
+Module EqdepTheory := EqdepTheory(Eq_rect_eq).
+Export EqdepTheory.
diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v
index b297770b8a..3c3b7bbfae 100755
--- a/theories/Logic/Eqdep.v
+++ b/theories/Logic/Eqdep.v
@@ -8,181 +8,27 @@
 
 (*i $Id$ i*)
 
-(** This file defines dependent equality and shows its equivalence with
-    equality on dependent pairs (inhabiting sigma-types). It axiomatizes
-    the invariance by substitution of reflexive equality proofs and 
-    shows the equivalence between the 4 following statements
+(** This file axiomatizes the invariance by substitution of reflexive
+    equality proofs [[Streicher93]] and exports its consequences, such
+    as the injectivity of the projection of the dependent pair.
 
-    - Invariance by Substitution of Reflexive Equality Proofs.
-    - Injectivity of Dependent Equality
-    - Uniqueness of Identity Proofs
-    - Uniqueness of Reflexive Identity Proofs
-    - Streicher's Axiom K
-
-  These statements are independent of the calculus of constructions [2].
-
-  References:
-
-  [1] T. Streicher, Semantical Investigations into Intensional Type Theory,
-      Habilitationsschrift, LMU München, 1993.
-  [2] M. Hofmann, T. Streicher, The groupoid interpretation of type theory,
-      Proceedings of the meeting Twenty-five years of constructive
-      type theory, Venice, Oxford University Press, 1998
+    [[Streicher93]] T. Streicher, Semantical Investigations into
+    Intensional Type Theory, Habilitationsschrift, LMU München, 1993.
 *)
 
-Section Dependent_Equality.
-
-Variable U : Type.
-Variable P : U -> Type.
-
-(** Dependent equality *)
-
-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.
-
-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.
+Require Export EqdepFacts.
 
-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.
-
-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.
-
-(** Invariance by Substitution of Reflexive Equality Proofs *)
+Module Eq_rect_eq.
 
 Axiom 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 is a consequence of *)
-(** Invariance by Substitution of Reflexive Equality Proof *)
-
-Lemma eq_dep1_eq : forall (p:U) (x y:P p), eq_dep1 p x p y -> x = y.
-Proof.
-simple destruct 1; intro.
-rewrite <- eq_rect_eq; auto.
-Qed.
-
-Lemma eq_dep_eq : forall (p:U) (x y:P p), eq_dep p x p y -> x = y.
-Proof.
-intros; apply eq_dep1_eq; apply eq_dep_dep1; trivial.
-Qed.
-
-End Dependent_Equality.
-
-(** Uniqueness of Identity Proofs (UIP) is a consequence of *)
-(** Injectivity of Dependent Equality *)
-
-Lemma UIP : forall (U:Type) (x y:U) (p1 p2:x = y), p1 = p2.
-Proof.
-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_refl : forall (U:Type) (x:U) (p:x = x), p = refl_equal x.
-Proof.
-intros; apply UIP.
-Qed.
-
-(** Streicher axiom K is a direct consequence of Uniqueness of
-    Reflexive Identity Proofs *)
-
-Lemma Streicher_K :
- forall (U:Type) (x:U) (P:x = x -> Prop),
-   P (refl_equal x) -> forall p:x = x, P p.
-Proof.
-intros; rewrite UIP_refl; assumption.
-Qed.
-
-(** We finally recover eq_rec_eq (alternatively eq_rect_eq) from K *)
-
-Lemma eq_rec_eq :
- forall (U:Type) (P:U -> Set) (p:U) (x:P p) (h:p = p), x = eq_rec p P x p h.
-Proof.
-intros.
-apply Streicher_K with (p := h).
-reflexivity.
-Qed.
-
-(** Dependent equality is equivalent to equality on dependent pairs *)
-
-Lemma equiv_eqex_eqdep :
- 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 U P p x q y.
-Proof.
-split. 
-(* -> *)
-intro H.
-change p with (projS1 (existS P p x)) in |- *.
-change x at 2 with (projS2 (existS P p x)) in |- *.
-rewrite H.
-apply eq_dep_intro.
-(* <- *)
-destruct 1; reflexivity.
-Qed.
-
-(** UIP implies the injectivity of equality on dependent pairs *)
-
-Lemma inj_pair2 :
- forall (U:Set) (P:U -> Set) (p:U) (x y:P p),
-   existS P p x = existS P p y -> x = y.
-Proof.
-intros.
-apply (eq_dep_eq U P).
-generalize (equiv_eqex_eqdep U P p p x y).
-simple induction 1.
-intros.
-auto.
-Qed.
+  forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
 
-(** UIP implies the injectivity of equality on dependent pairs *)
+End Eq_rect_eq.
 
-Lemma inj_pairT2 :
- forall (U:Type) (P:U -> Type) (p:U) (x y:P p),
-   existT P p x = existT P p y -> x = y.
-Proof.
-intros.
-apply (eq_dep_eq U P).
-change p at 1 with (projT1 (existT P p x)) in |- *.
-change x at 2 with (projT2 (existT P p x)) in |- *.
-rewrite H.
-apply eq_dep_intro.
-Qed.
+Module EqdepTheory := EqdepTheory(Eq_rect_eq).
+Export EqdepTheory.
 
-(** The main results to be exported *)
+(** Exported hints *)
 
-Hint Resolve eq_dep_intro eq_dep_eq: core v62.
-Hint Immediate eq_dep_sym: core v62.
+Hint Resolve eq_dep_eq: core v62.
 Hint Resolve inj_pair2 inj_pairT2: core.
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
new file mode 100644
index 0000000000..32237a0c90
--- /dev/null
+++ b/theories/Logic/EqdepFacts.v
@@ -0,0 +1,347 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+(** This file defines dependent equality and shows its equivalence with
+    equality on dependent pairs (inhabiting sigma-types). It derives
+    the consequence of axiomatizing the invariance by substitution of
+    reflexive equality proofs and shows the equivalence between the 4
+    following statements
+
+    - Invariance by Substitution of Reflexive Equality Proofs.
+    - Injectivity of Dependent Equality
+    - Uniqueness of Identity Proofs
+    - Uniqueness of Reflexive Identity Proofs
+    - Streicher's Axiom K
+
+  These statements are independent of the calculus of constructions [2].
+
+  References:
+
+  [1] T. Streicher, Semantical Investigations into Intensional Type Theory,
+      Habilitationsschrift, LMU München, 1993.
+  [2] M. Hofmann, T. Streicher, The groupoid interpretation of type theory,
+      Proceedings of the meeting Twenty-five years of constructive
+      type theory, Venice, Oxford University Press, 1998
+
+Table of contents:
+
+A. Definition of dependent equality and equivalence with equality
+
+B. Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K
+
+C. 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 *)
+
+Section Dependent_Equality.
+
+Variable U : Type.
+Variable P : U -> Type.
+
+(** Dependent equality *)
+
+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.
+
+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_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.
+
+(** 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 :=
+    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.
+
+End Dependent_Equality.
+
+Implicit Arguments eq_dep [U P].
+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.
+Proof.
+  intros.
+  dependent rewrite H.
+  apply eq_dep_intro.
+Qed.
+
+Lemma equiv_eqex_eqdep :
+ 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. 
+  (* -> *)
+  apply eq_sigS_eq_dep.
+  (* <- *)
+  destruct 1; reflexivity.
+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.
+Proof.
+  intros.
+  dependent rewrite H.
+  apply eq_dep_intro.
+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.
+Proof.
+  destruct 1; reflexivity.
+Qed.
+
+(** Exported hints *)
+
+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          *)
+
+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.
+
+(** 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]):
+
+   [Definition Eq_rec_eq :=
+      forall (P:U -> Set) (p:U) (x:P p) (h:p = p), x = eq_rec p P x p h.]
+
+    Typically, [eq_rect_eq] allows to prove UIP and Streicher's K what
+    does not seem possible with [eq_rec_eq]. In particular, the proof of [UIP]
+    requires to use [eq_rect_eq] on [fun y -> x=y] which is in [Type] but not
+    in [Set].  
+*)
+
+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.
+ 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_sigS_eq_dep.
+  assumption.
+Qed.
+
+End Corollaries.
+
+(************************************************************************)
+(** *** C. Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq *)
+
+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.
+
+End EqdepElimination.
+
+Module EqdepTheory (M:EqdepElimination).
+
+Section Axioms.
+
+Variable U:Type.
+
+(** Invariance by Substitution of Reflexive Equality Proofs *)
+
+Lemma eq_rect_eq :
+  forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
+Proof M.eq_rect_eq U.
+
+(** Injectivity of Dependent Equality *)
+
+Lemma eq_dep_eq : forall (P:U->Type) (p:U) (x y:P p), eq_dep p x p y -> x = y.
+Proof (eq_rect_eq__eq_dep_eq U eq_rect_eq).
+
+(** Uniqueness of Identity Proofs (UIP) is a consequence of *)
+(** Injectivity of Dependent Equality *)
+
+Lemma UIP : forall (x y:U) (p1 p2:x = y), p1 = p2.
+Proof (eq_dep_eq__UIP U eq_dep_eq).
+
+(** Uniqueness of Reflexive Identity Proofs is a direct instance of UIP *)
+
+Lemma UIP_refl : forall (x:U) (p:x = x), p = refl_equal x.
+Proof (UIP__UIP_refl U UIP).
+
+(** Streicher's axiom K is a direct consequence of Uniqueness of
+    Reflexive Identity Proofs *)
+
+Lemma Streicher_K :
+  forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
+Proof (UIP_refl__Streicher_K U UIP_refl).
+
+End Axioms.
+
+(** UIP implies the injectivity of equality on dependent pairs in Type *)
+
+Lemma inj_pairT2 :
+ forall (U:Type) (P:U -> Type) (p:U) (x y:P p),
+   existT P p x = existT P p y -> x = y.
+Proof (fun U => eq_dep_eq__inj_pairT2 U (eq_dep_eq U)).
+
+(** UIP implies the injectivity of equality on dependent pairs in Set *)
+
+Lemma inj_pair2 :
+ forall (U:Set) (P:U -> Set) (p:U) (x y:P p),
+   existS P p x = existS P p y -> x = y.
+Proof (fun U => eq_dep_eq__inj_pair2 U (eq_dep_eq U)).
+
+End EqdepTheory.
+
+Implicit Arguments eq_dep [].
+Implicit Arguments eq_dep1 [].
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 29a08a2e4b..3cb9419710 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -8,23 +8,34 @@
 
 (*i $Id$ 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.
-   A corollary of this theorem is the equality of the right projections
-   of two equal dependent pairs.
+(** 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.
+    A corollary of this theorem is the equality of the right projections
+    of two equal dependent pairs.
 
-   Author:   Thomas Kleymann |<tms@dcs.ed.ac.uk>| in Lego
-             adapted to Coq by B. Barras
+    Author:   Thomas Kleymann |<tms@dcs.ed.ac.uk>| in Lego
+              adapted to Coq by B. Barras
 
-   Credit:   Proofs up to [K_dec] follows an outline by Michael Hedberg
-*)
+    Credit:   Proofs up to [K_dec] follow an outline by Michael Hedberg
+
+Table of contents:
+
+A. Streicher's K and injectivity of dependent pair hold on decidable types
 
+B.1. Definition of the functor that builds properties of dependent equalities
+     from a proof of decidability of equality for a set in Type
 
-(** We need some dependent elimination schemes *)
+B.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 *)
 
 Set Implicit Arguments.
 
-Section DecidableEqDep.
+Section EqdepDec.
 
   Variable A : Type.
 
@@ -84,7 +95,6 @@ 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 :=
@@ -114,20 +124,173 @@ case H.
 reflexivity.
 Qed.
 
-End DecidableEqDep.
+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.
+Qed.
 
-  (** We deduce the [K] axiom for (decidable) Set *)
   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.
-intros.
-elim p using K_dec.
-intros.
-case (H x0 y); intros.
-elim e; left; reflexivity.
-
-right; red in |- *; intro neq; apply n; elim neq; reflexivity.
+  Proof fun A => K_dec_type (A:=A).
 
-trivial.
+  (** 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)).
 Qed.
+
+Unset Implicit Arguments.
+
+(************************************************************************)
+(** *** B.1. 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}.
+
+End DecidableType.
+
+(** The module [DecidableEqDep] collects equality properties for decidable 
+    set in [Type] *)
+
+Module DecidableEqDep (M:DecidableType).
+
+  Import M.
+
+  (** Invariance by Substitution of Reflexive Equality Proofs *)
+
+  Lemma eq_rect_eq :
+    forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
+  Proof eq_rect_eq_dec eq_dec.
+
+  (** Injectivity of Dependent Equality *)
+
+  Theorem eq_dep_eq :
+    forall (P:U->Type) (p:U) (x y:P p), eq_dep U P p x p y -> x = y.
+  Proof (eq_rect_eq__eq_dep_eq U eq_rect_eq).
+
+  (** Uniqueness of Identity Proofs (UIP) *)
+
+  Lemma UIP : forall (x y:U) (p1 p2:x = y), p1 = p2.
+  Proof (eq_dep_eq__UIP U eq_dep_eq).
+
+  (** Uniqueness of Reflexive Identity Proofs *)
+
+  Lemma UIP_refl : forall (x:U) (p:x = x), p = refl_equal x.
+  Proof (UIP__UIP_refl U UIP).
+
+  (** Streicher's axiom K *)
+
+  Lemma Streicher_K :
+    forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
+  Proof (K_dec_type eq_dec).
+
+  (** Injectivity of equality on dependent pairs in [Type] *)
+
+  Lemma inj_pairT2 :
+    forall (P:U -> Type) (p:U) (x y:P p),
+      existT P p x = existT P p y -> x = y.
+  Proof eq_dep_eq__inj_pairT2 U eq_dep_eq.
+
+  (** Proof-irrelevance on subsets of decidable sets *)
+
+  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.
+  Qed.
+
+End DecidableEqDep.
+
+(************************************************************************)
+(** *** B.2 Definition of the functor that builds properties of dependent equalities on decidable sets in Set *)
+
+(** The signature of decidable sets in [Set] *)
+
+Module Type DecidableSet.
+
+  Parameter U:Set.
+  Axiom eq_dec : forall x y:U, {x = y} + {x <> y}.
+
+End DecidableSet.
+
+(** The module [DecidableEqDepSet] collects equality properties for decidable 
+    set in [Set] *)
+
+Module DecidableEqDepSet (M:DecidableSet).
+
+  Import M.
+  Module N:=DecidableEqDep(M).
+
+  (** Invariance by Substitution of Reflexive Equality Proofs *)
+
+  Lemma eq_rect_eq :
+    forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
+  Proof eq_rect_eq_dec eq_dec.
+
+  (** Injectivity of Dependent Equality *)
+
+  Theorem eq_dep_eq :
+    forall (P:U->Type) (p:U) (x y:P p), eq_dep U P p x p y -> x = y.
+  Proof N.eq_dep_eq.
+
+  (** Uniqueness of Identity Proofs (UIP) *)
+
+  Lemma UIP : forall (x y:U) (p1 p2:x = y), p1 = p2.
+  Proof N.UIP.
+
+  (** Uniqueness of Reflexive Identity Proofs *)
+
+  Lemma UIP_refl : forall (x:U) (p:x = x), p = refl_equal x.
+  Proof N.UIP_refl.
+
+  (** Streicher's axiom K *)
+
+  Lemma Streicher_K :
+    forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
+  Proof N.Streicher_K.
+
+  (** Injectivity of equality on dependent pairs with second component
+      in [Type] *)
+
+  Lemma inj_pairT2 :
+    forall (P:U -> Type) (p:U) (x y:P p),
+      existT P p x = existT P p y -> x = y.
+  Proof N.inj_pairT2.
+
+  (** Proof-irrelevance on subsets of decidable sets *)
+
+  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.
+  Proof N.inj_pairP2.
+
+  (** Injectivity of equality on dependent pairs in [Set] *)
+
+  Lemma inj_pair2 :
+    forall (P:U -> Set) (p:U) (x y:P p),
+      existS P p x = existS P p y -> x = y.
+  Proof eq_dep_eq__inj_pair2 U N.eq_dep_eq.
+
+End DecidableEqDepSet.
diff --git a/theories/Logic/ProofIrrelevance.v b/theories/Logic/ProofIrrelevance.v
index 7c8869d5d8..44ab9a2eef 100644
--- a/theories/Logic/ProofIrrelevance.v
+++ b/theories/Logic/ProofIrrelevance.v
@@ -6,110 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** This is a proof in the pure Calculus of Construction that
-    classical logic in Prop + dependent elimination of disjunction entails
-    proof-irrelevance.
+(** This file axiomatizes proof-irrelevance and derives some consequences *)
 
-    Since, dependent elimination is derivable in the Calculus of
-    Inductive Constructions (CCI), we get proof-irrelevance from classical
-    logic in the CCI.
+Require Import ProofIrrelevanceFacts.
 
-    Reference:
+Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.
 
-    - [Coquand] T. Coquand, "Metamathematical Investigations of a
-      Calculus of Constructions", Proceedings of Logic in Computer Science
-      (LICS'90), 1990.
+Module PI. Definition proof_irrelevance := proof_irrelevance. End PI.
 
-    Proof skeleton: classical logic + dependent elimination of
-    disjunction + discrimination of proofs implies the existence of a
-    retract from [Prop] into [bool], hence inconsistency by encoding any
-    paradox of system U- (e.g. Hurkens' paradox).
-*)
-
-Require Import Hurkens.
-
-Section Proof_irrelevance_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 :
-    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 :
-    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 :
-    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.
-    trivial.
-  apply (paradox B p2b b2p (p2p2 H) p2p1).
-Qed.
-
-End Proof_irrelevance_CC.
-
-
-(** The Calculus of Inductive Constructions (CCI) enjoys dependent
-    elimination, hence classical logic in CCI entails proof-irrelevance.
-*)
-
-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.
-
-End Proof_irrelevance_CCI.
-
-(** Remark: in the Set-impredicative CCI, Hurkens' paradox still holds with
-    [bool] in [Set] and since [~true=false] for [true] and [false]
-    in [bool] from [Set], we get the inconsistency of
-    [em : forall A:Prop, {A}+{~A}] in the Set-impredicative CCI.
-*)
+Module ProofIrrelevanceTheory := ProofIrrelevanceTheory(PI).
+Export ProofIrrelevanceTheory.
diff --git a/theories/Logic/ProofIrrelevanceFacts.v b/theories/Logic/ProofIrrelevanceFacts.v
new file mode 100644
index 0000000000..dd3178ebec
--- /dev/null
+++ b/theories/Logic/ProofIrrelevanceFacts.v
@@ -0,0 +1,62 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** This defines the functor that build consequences of proof-irrelevance *)
+
+Require Export EqdepFacts.
+
+Module Type ProofIrrelevance.
+
+  Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.
+
+End ProofIrrelevance.
+
+Module ProofIrrelevanceTheory (M:ProofIrrelevance).
+
+  (** Proof-irrelevance implies uniqueness of reflexivity proofs *)
+
+  Module Eq_rect_eq.
+    Lemma 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.
+    Proof.
+      intros; rewrite M.proof_irrelevance with (p1:=h) (p2:=refl_equal p).
+      reflexivity.
+    Qed.
+  End Eq_rect_eq.
+
+  (** Export the theory of injective dependent elimination *)
+
+  Module EqdepTheory := EqdepTheory(Eq_rect_eq).
+  Export EqdepTheory.
+
+  Scheme eq_indd := Induction for eq Sort Prop.
+
+  (** We derive the irrelevance of the membership property for subsets *)
+
+  Lemma subset_eq_compat :
+    forall (U:Set) (P:U->Prop) (x y:U) (p:P x) (q:P y),
+      x = y -> exist P x p = exist P y q.
+  Proof.
+    intros.
+    rewrite M.proof_irrelevance with (p1:=q) (p2:=eq_rect x P p y H).
+    elim H using eq_indd.
+    reflexivity.
+  Qed.
+
+  Lemma subsetT_eq_compat :
+    forall (U:Type) (P:U->Prop) (x y:U) (p:P x) (q:P y),
+      x = y -> existT P x p = existT P y q.
+  Proof.
+    intros.
+    rewrite M.proof_irrelevance with (p1:=q) (p2:=eq_rect x P p y H).
+    elim H using eq_indd.
+    reflexivity.
+  Qed.
+
+End ProofIrrelevanceTheory.