1 files changed, 0 insertions, 56 deletions
diff --git a/theories7/Wellfounded/Disjoint_Union.v b/theories7/Wellfounded/Disjoint_Union.v
deleted file mode 100644
index 04930170..00000000
--- a/theories7/Wellfounded/Disjoint_Union.v
+++ /dev/null
@@ -1,56 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: Disjoint_Union.v,v 1.1.2.1 2004/07/16 19:31:41 herbelin Exp $ i*)
-
-(** Author: Cristina Cornes
-    From : Constructing Recursion Operators in Type Theory                 
-           L. Paulson  JSC (1986) 2, 325-355 *) 
-
-Require Relation_Operators.
-
-Section Wf_Disjoint_Union.
-Variable 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: (x:A)(Acc A leA x)->(Acc A+B Le_AsB (inl A B x)).
-Proof.
- NewInduction 1.
- Apply Acc_intro;Intros y H2.
- Inversion_clear H2.
- Auto with sets.
-Qed.
-
-Lemma acc_B_sum: (well_founded A leA) ->(x:B)(Acc B leB x)
-                        ->(Acc A+B Le_AsB (inr A B x)).
-Proof.
- NewInduction 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 A leA) 
-    -> (well_founded B leB) -> (well_founded A+B Le_AsB).
-Proof.
- Intros.
- Unfold well_founded .
- NewDestruct 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.