1 files changed, 37 insertions, 37 deletions
diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v
index 940569bd..1e22730b 100644
--- a/theories/Wellfounded/Disjoint_Union.v
+++ b/theories/Wellfounded/Disjoint_Union.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Disjoint_Union.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: Disjoint_Union.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 (** Author: Cristina Cornes
     From : Constructing Recursion Operators in Type Theory                 
@@ -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