diff options
Diffstat (limited to 'theories/Logic/ClassicalChoice.v')
| -rw-r--r-- | theories/Logic/ClassicalChoice.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v index 80bbce461c..7b6fcdf53d 100644 --- a/theories/Logic/ClassicalChoice.v +++ b/theories/Logic/ClassicalChoice.v @@ -23,8 +23,8 @@ Require Import ChoiceFacts. Theorem 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)). + (forall x:A, exists y : B, R x y) -> + exists f : A -> B, (forall x:A, R x (f x)). Proof. apply description_rel_choice_imp_funct_choice. exact description. |