diff options
Diffstat (limited to 'theories/Logic/ClassicalDescription.v')
| -rw-r--r-- | theories/Logic/ClassicalDescription.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v index dad60fb77..2b9df6d97 100644 --- a/theories/Logic/ClassicalDescription.v +++ b/theories/Logic/ClassicalDescription.v @@ -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). |