1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(** This defines the functor that build consequences of proof-irrelevance *)
11
Require Export EqdepFacts.
13
Module Type ProofIrrelevance.
15
Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.
19
Module ProofIrrelevanceTheory (M:ProofIrrelevance).
21
(** Proof-irrelevance implies uniqueness of reflexivity proofs *)
25
forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p),
26
x = eq_rect p Q x p h.
28
intros; rewrite M.proof_irrelevance with (p1:=h) (p2:=refl_equal p).
33
(** Export the theory of injective dependent elimination *)
35
Module EqdepTheory := EqdepTheory(Eq_rect_eq).
38
Scheme eq_indd := Induction for eq Sort Prop.
40
(** We derive the irrelevance of the membership property for subsets *)
42
Lemma subset_eq_compat :
43
forall (U:Set) (P:U->Prop) (x y:U) (p:P x) (q:P y),
44
x = y -> exist P x p = exist P y q.
47
rewrite M.proof_irrelevance with (p1:=q) (p2:=eq_rect x P p y H).
52
Lemma subsetT_eq_compat :
53
forall (U:Type) (P:U->Prop) (x y:U) (p:P x) (q:P y),
54
x = y -> existT P x p = existT P y q.
57
rewrite M.proof_irrelevance with (p1:=q) (p2:=eq_rect x P p y H).
62
End ProofIrrelevanceTheory.