diff options
Diffstat (limited to 'theories/Sets/Finite_sets.v')
| -rw-r--r-- | theories/Sets/Finite_sets.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v index a75c3b767..019c25a55 100644 --- a/theories/Sets/Finite_sets.v +++ b/theories/Sets/Finite_sets.v @@ -52,7 +52,7 @@ Require Import Constructive_sets. Section Ensembles_finis_facts. Variable U : Type. - + Lemma cardinal_invert : forall (X:Ensemble U) (p:nat), cardinal U X p -> |