diff options
Diffstat (limited to 'theories/Sets/Finite_sets_facts.v')
| -rwxr-xr-x | theories/Sets/Finite_sets_facts.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v index 2849bce6c..f394b2e5a 100755 --- a/theories/Sets/Finite_sets_facts.v +++ b/theories/Sets/Finite_sets_facts.v @@ -40,7 +40,7 @@ Section Finite_sets_facts. Variable U : Type. Lemma finite_cardinal : - forall X:Ensemble U, Finite U X -> exists n : nat | cardinal U X n. + forall X:Ensemble U, Finite U X -> exists n : nat, cardinal U X n. Proof. induction 1 as [| A _ [n H]]. exists 0; auto with sets. |