Mise en forme des theories

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 36 insertions, 37 deletions

diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v
index 03560253f..b1cb63be1 100644
--- a/theories/Wellfounded/Well_Ordering.v
+++ b/theories/Wellfounded/Well_Ordering.v
@@ -15,58 +15,57 @@
 Require Import Eqdep.
 
 Section WellOrdering.
-Variable A : Set.
-Variable B : A -> Set. 
-
-Inductive WO : Set :=
+  Variable A : Set.
+  Variable B : A -> Set. 
+  
+  Inductive WO : Set :=
     sup : forall (a:A) (f:B a -> WO), WO.
 
 
-Inductive le_WO : WO -> WO -> Prop :=
+  Inductive le_WO : WO -> WO -> Prop :=
     le_sup : forall (a:A) (f:B a -> WO) (v:B a), le_WO (f v) (sup a f).
  
-
-Theorem wf_WO : well_founded le_WO.
-Proof.
- unfold well_founded in |- *; intro.
- apply Acc_intro.
- elim a.
- intros.
- inversion H0.
- apply Acc_intro.
- generalize H4; generalize H1; generalize f0; generalize v.
- rewrite H3.
- intros.
- apply (H v0 y0).
- cut (f = f1).
- intros E; rewrite E; auto.
- symmetry  in |- *.
- apply (inj_pair2 A (fun a0:A => B a0 -> WO) a0 f1 f H5).
-Qed.
+  Theorem wf_WO : well_founded le_WO.
+  Proof.
+    unfold well_founded in |- *; intro.
+    apply Acc_intro.
+    elim a.
+    intros.
+    inversion H0.
+    apply Acc_intro.
+    generalize H4; generalize H1; generalize f0; generalize v.
+    rewrite H3.
+    intros.
+    apply (H v0 y0).
+    cut (f = f1).
+    intros E; rewrite E; auto.
+    symmetry  in |- *.
+    apply (inj_pair2 A (fun a0:A => B a0 -> WO) a0 f1 f H5).
+  Qed.
 
 End WellOrdering.
 
 
 Section Characterisation_wf_relations.
 
-(** Wellfounded relations are the inverse image of wellordering types *)
-(*  in course of development                                          *)
+  (** Wellfounded relations are the inverse image of wellordering types *)
+  (*  in course of development                                          *)
 
 
-Variable A : Set.
-Variable leA : A -> A -> Prop.
+  Variable A : Set.
+  Variable leA : A -> A -> Prop.
 
-Definition B (a:A) := {x : A | leA x a}.
+  Definition B (a:A) := {x : A | leA x a}.
 
-Definition wof : well_founded leA -> A -> WO A B.
-Proof.
- intros.
- apply (well_founded_induction H (fun a:A => WO A B)); auto.
- intros.
- apply (sup A B x).
- unfold B at 1 in |- *.
- destruct 1 as [x0].
- apply (H1 x0); auto.
+  Definition wof : well_founded leA -> A -> WO A B.
+  Proof.
+    intros.
+    apply (well_founded_induction H (fun a:A => WO A B)); auto.
+    intros.
+    apply (sup A B x).
+    unfold B at 1 in |- *.
+    destruct 1 as [x0].
+    apply (H1 x0); auto.
 Qed.
 
 End Characterisation_wf_relations.
\ No newline at end of file