From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 theories/Logic/ClassicalEpsilon.v | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

(limited to 'theories/Logic/ClassicalEpsilon.v')

diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v
index 2a4de511..cee55dc8 100644
--- a/theories/Logic/ClassicalEpsilon.v
+++ b/theories/Logic/ClassicalEpsilon.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ClassicalEpsilon.v 10170 2007-10-03 14:41:25Z herbelin $ i*)
+(*i $Id$ i*)
 
 (** This file provides classical logic and indefinite description under
     the form of Hilbert's epsilon operator *)
@@ -22,11 +23,11 @@ Require Import ChoiceFacts.
 Set Implicit Arguments.
 
 Axiom constructive_indefinite_description :
-  forall (A : Type) (P : A->Prop), 
+  forall (A : Type) (P : A->Prop),
     (exists x, P x) -> { x : A | P x }.
 
 Lemma constructive_definite_description :
-  forall (A : Type) (P : A->Prop), 
+  forall (A : Type) (P : A->Prop),
     (exists! x, P x) -> { x : A | P x }.
 Proof.
   intros; apply constructive_indefinite_description; firstorder.
@@ -34,18 +35,18 @@ Qed.
 
 Theorem excluded_middle_informative : forall P:Prop, {P} + {~ P}.
 Proof.
-  apply 
-    (constructive_definite_descr_excluded_middle 
+  apply
+    (constructive_definite_descr_excluded_middle
       constructive_definite_description classic).
 Qed.
 
-Theorem classical_indefinite_description : 
+Theorem classical_indefinite_description :
   forall (A : Type) (P : A->Prop), inhabited A ->
     { 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 
+  apply constructive_indefinite_description
     with (P:= fun x => (exists x, P x) -> P x).
   destruct Hex as (x,Hx).
     exists x; intros _; exact Hx.
@@ -60,7 +61,7 @@ Defined.
 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) : 
+Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) :
   (exists x, P x) -> P (epsilon i P)
   := proj2_sig (classical_indefinite_description P i).
 
@@ -74,9 +75,9 @@ Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) :
 
 (** 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) *)
+    (proof idea kindly provided by Pierre Castéran) *)
 
-Lemma epsilon_inh_irrelevance : 
+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.
-- 
cgit v1.2.3