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, 36 deletions

diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v
index 76c9ad443..c82549e37 100644
--- a/theories/Wellfounded/Disjoint_Union.v
+++ b/theories/Wellfounded/Disjoint_Union.v
@@ -15,41 +15,41 @@
 Require Import Relation_Operators.
 
 Section Wf_Disjoint_Union.
-Variables A B : Set.
-Variable leA : A -> A -> Prop.
-Variable leB : B -> B -> Prop.
-
-Notation Le_AsB := (le_AsB A B leA leB).
-
-Lemma acc_A_sum : forall x:A, Acc leA x -> Acc Le_AsB (inl B x).
-Proof.
- induction 1.
- apply Acc_intro; intros y H2.
- inversion_clear H2.
- auto with sets.
-Qed.
-
-Lemma acc_B_sum :
- well_founded leA -> forall x:B, Acc leB x -> Acc Le_AsB (inr A x).
-Proof.
- induction 2.
- apply Acc_intro; intros y H3.
- inversion_clear H3; auto with sets.
- apply acc_A_sum; auto with sets.
-Qed.
-
-
-Lemma wf_disjoint_sum :
- well_founded leA -> well_founded leB -> well_founded Le_AsB.
-Proof.
- intros.
- unfold well_founded in |- *.
- destruct a as [a| b].
- apply (acc_A_sum a).
- apply (H a).
-
- apply (acc_B_sum H b).
- apply (H0 b).
-Qed.
+  Variables A B : Set.
+  Variable leA : A -> A -> Prop.
+  Variable leB : B -> B -> Prop.
+
+  Notation Le_AsB := (le_AsB A B leA leB).
+  
+  Lemma acc_A_sum : forall x:A, Acc leA x -> Acc Le_AsB (inl B x).
+  Proof.
+    induction 1.
+    apply Acc_intro; intros y H2.
+    inversion_clear H2.
+    auto with sets.
+  Qed.
+
+  Lemma acc_B_sum :
+    well_founded leA -> forall x:B, Acc leB x -> Acc Le_AsB (inr A x).
+  Proof.
+    induction 2.
+    apply Acc_intro; intros y H3.
+    inversion_clear H3; auto with sets.
+    apply acc_A_sum; auto with sets.
+  Qed.
+
+
+  Lemma wf_disjoint_sum :
+    well_founded leA -> well_founded leB -> well_founded Le_AsB.
+  Proof.
+    intros.
+    unfold well_founded in |- *.
+    destruct a as [a| b].
+    apply (acc_A_sum a).
+    apply (H a).
+    
+    apply (acc_B_sum H b).
+    apply (H0 b).
+  Qed.
 
 End Wf_Disjoint_Union.
\ No newline at end of file