1 files changed, 15 insertions, 27 deletions
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index 7053266a..1f1c34bf 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ClassicalDescription.v 8892 2006-06-04 17:59:53Z herbelin $ i*)
+(*i $Id: ClassicalDescription.v 9514 2007-01-22 14:58:50Z herbelin $ i*)
 
 (** This file provides classical logic and definite description *)
 
@@ -57,14 +57,11 @@ Definition iota_spec (A : Type) (i:inhabited A) (P : A->Prop) :
   (exists! x:A, P x) -> P (iota i P)
   := proj2_sig (classical_definite_description P i).
 
-(** Weaker lemmas (compatibility lemmas) *)
-
-Unset Implicit Arguments.
-
-Lemma dependent_description :
-    forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
-      (forall x:A, exists! y : B x, R x y) ->
-      (exists f : (forall x:A, B x), forall x:A, R x (f x)).
+(** Axiom of unique "choice" (functional reification of functional relations) *)
+Theorem dependent_unique_choice :
+  forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
+    (forall x:A, exists! y : B x, R x y) ->
+    (exists f : (forall x:A, B x), forall x:A, R x (f x)).
 Proof.
 intros A B R H.
 assert (Hexuni:forall x, exists! y, R x y).
@@ -74,27 +71,18 @@ intro x.
 apply (proj2_sig (constructive_definite_description (R x) (Hexuni x))).
 Qed.
 
-Theorem description :
- forall (A B:Type) (R:A -> B -> Prop),
-   (forall x : A,  exists! y : B, R x y) ->
-   (exists f : A->B, forall x:A, R x (f x)).
+Theorem unique_choice :
+  forall (A B:Type) (R:A -> B -> Prop),
+    (forall x:A,  exists! y : B, R x y) ->
+    (exists f : A -> B, forall x:A, R x (f x)).
 Proof.
 intros A B.
-apply (dependent_description A (fun _ => B)).
+apply dependent_unique_choice with (B:=fun _:A => B).
 Qed.
 
-(** Axiom of unique "choice" (functional reification of functional relations) *)
+(** Compatibility lemmas *)
 
-Set Implicit Arguments.
-
-Require Import Setoid.
+Unset Implicit Arguments.
 
-Theorem unique_choice :
- forall (A B:Type) (R:A -> B -> Prop),
-   (forall x:A,  exists! y : B, R x y) ->
-   (exists f : A -> B, forall x:A, R x (f x)).
-Proof.
-intros A B R H.
-apply (description A B).
-intro x. apply H.
-Qed.
+Definition dependent_description := dependent_unique_choice.
+Definition description := unique_choice.