1 files changed, 0 insertions, 72 deletions
diff --git a/theories7/Wellfounded/Well_Ordering.v b/theories7/Wellfounded/Well_Ordering.v
deleted file mode 100644
index 5c2b2405..00000000
--- a/theories7/Wellfounded/Well_Ordering.v
+++ /dev/null
@@ -1,72 +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: Well_Ordering.v,v 1.1.2.1 2004/07/16 19:31:42 herbelin Exp $ i*)
-
-(** Author: Cristina Cornes.
-    From: Constructing Recursion Operators in Type Theory
-    L. Paulson  JSC (1986) 2, 325-355 *)
-
-Require Eqdep.
-
-Section WellOrdering.
-Variable A:Set.
-Variable B:A->Set. 
-
-Inductive WO : Set :=
-   sup : (a:A)(f:(B a)->WO)WO.
-
-
-Inductive le_WO  : WO->WO->Prop :=
-  le_sup : (a:A)(f:(B a)->WO)(v:(B a)) (le_WO  (f v) (sup a f)).
- 
-
-Theorem wf_WO : (well_founded WO le_WO ).
-Proof.
- Unfold well_founded ;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 (eq ? f f1).
- Intros E;Rewrite -> E;Auto.
- Symmetry.
- Apply (inj_pair2 A [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                                          *)
-
-
-Variable A:Set.
-Variable leA:A->A->Prop.
-
-Definition B:= [a:A] {x:A | (leA x a)}.
-
-Definition  wof: (well_founded A leA)-> A-> (WO A B).
-Proof.
- Intros.
- Apply (well_founded_induction A leA H [a:A](WO A B));Auto.
- Intros.
- Apply (sup A B x).
- Unfold 1 B .
- NewDestruct 1 as [x0].
- Apply (H1 x0);Auto.
-Qed.
-
-End Characterisation_wf_relations.