1 files changed, 33 insertions, 33 deletions
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v
index 47b41ec3..f5eae4ed 100644
--- a/theories/Sets/Finite_sets.v
+++ b/theories/Sets/Finite_sets.v
@@ -24,22 +24,22 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Finite_sets.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Finite_sets.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 Require Import Ensembles.
 
 Section Ensembles_finis.
-Variable U : Type.
+  Variable U : Type.
 
-Inductive Finite : Ensemble U -> Prop :=
-  | Empty_is_finite : Finite (Empty_set U)
-  | Union_is_finite :
+  Inductive Finite : Ensemble U -> Prop :=
+    | Empty_is_finite : Finite (Empty_set U)
+    | Union_is_finite :
       forall A:Ensemble U,
         Finite A -> forall x:U, ~ In U A x -> Finite (Add U A x).
 
-Inductive cardinal : Ensemble U -> nat -> Prop :=
-  | card_empty : cardinal (Empty_set U) 0
-  | card_add :
+  Inductive cardinal : Ensemble U -> nat -> Prop :=
+    | card_empty : cardinal (Empty_set U) 0
+    | card_add :
       forall (A:Ensemble U) (n:nat),
         cardinal A n -> forall x:U, ~ In U A x -> cardinal (Add U A x) (S n).
 
@@ -51,31 +51,31 @@ Hint Resolve card_empty card_add: sets v62.
 Require Import Constructive_sets.
 
 Section Ensembles_finis_facts.
-Variable U : Type.
+  Variable U : Type.
+  
+  Lemma cardinal_invert :
+    forall (X:Ensemble U) (p:nat),
+      cardinal U X p ->
+      match p with
+	| O => X = Empty_set U
+	| S n =>
+          exists A : _,
+            (exists x : _, X = Add U A x /\ ~ In U A x /\ cardinal U A n)
+      end.
+  Proof.
+    induction 1; simpl in |- *; auto.
+    exists A; exists x; auto.
+  Qed.
 
-Lemma cardinal_invert :
- forall (X:Ensemble U) (p:nat),
-   cardinal U X p ->
-   match p with
-   | O => X = Empty_set U
-   | S n =>
-        exists A : _,
-         (exists x : _, X = Add U A x /\ ~ In U A x /\ cardinal U A n)
-   end.
-Proof.
-induction 1; simpl in |- *; auto.
-exists A; exists x; auto.
-Qed.
-
-Lemma cardinal_elim :
- forall (X:Ensemble U) (p:nat),
-   cardinal U X p ->
-   match p with
-   | O => X = Empty_set U
-   | S n => Inhabited U X
-   end.
-Proof.
-intros X p C; elim C; simpl in |- *; trivial with sets.
-Qed.
+  Lemma cardinal_elim :
+    forall (X:Ensemble U) (p:nat),
+      cardinal U X p ->
+      match p with
+	| O => X = Empty_set U
+	| S n => Inhabited U X
+      end.
+  Proof.
+    intros X p C; elim C; simpl in |- *; trivial with sets.
+  Qed.
 
 End Ensembles_finis_facts.