diff options
Diffstat (limited to 'theories/Logic/ClassicalDescription.v')
| -rw-r--r-- | theories/Logic/ClassicalDescription.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v index 31c41120..2b9df6d9 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 11481 2008-10-20 19:23:51Z herbelin $ i*) +(*i $Id$ i*) (** This file provides classical logic and definite description, which is equivalent to providing classical logic and Church's iota operator *) @@ -30,12 +30,12 @@ Axiom constructive_definite_description : 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_definite_description : +Theorem classical_definite_description : forall (A : Type) (P : A->Prop), inhabited A -> { x : A | (exists! x : A, P x) -> P x }. Proof. @@ -54,7 +54,7 @@ Qed. Definition iota (A : Type) (i:inhabited A) (P : A->Prop) : A := proj1_sig (classical_definite_description P i). -Definition iota_spec (A : Type) (i:inhabited A) (P : A->Prop) : +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). |