1 files changed, 0 insertions, 162 deletions
diff --git a/theories7/Sets/Constructive_sets.v b/theories7/Sets/Constructive_sets.v
deleted file mode 100755
index 35c88e9d..00000000
--- a/theories7/Sets/Constructive_sets.v
+++ /dev/null
@@ -1,162 +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        *)
-(************************************************************************)
-(****************************************************************************)
-(*                                                                          *)
-(*                         Naive Set Theory in Coq                          *)
-(*                                                                          *)
-(*                     INRIA                        INRIA                   *)
-(*              Rocquencourt                        Sophia-Antipolis        *)
-(*                                                                          *)
-(*                                 Coq V6.1                                 *)
-(*									    *)
-(*			         Gilles Kahn 				    *)
-(*				 Gerard Huet				    *)
-(*									    *)
-(*									    *)
-(*                                                                          *)
-(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks  *)
-(* to the Newton Institute for providing an exceptional work environment    *)
-(* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
-(****************************************************************************)
-
-(*i $Id: Constructive_sets.v,v 1.1.2.1 2004/07/16 19:31:38 herbelin Exp $ i*)
-
-Require Export Ensembles.
-
-Section Ensembles_facts.
-Variable U: Type.
-
-Lemma Extension: (B, C: (Ensemble U)) B == C -> (Same_set U B C).
-Proof.
-Intros B C H'; Rewrite H'; Auto with sets.
-Qed.
-
-Lemma Noone_in_empty: (x: U) ~ (In U (Empty_set U) x).
-Proof.
-Red; NewDestruct 1.
-Qed.
-Hints Resolve Noone_in_empty.
-
-Lemma Included_Empty: (A: (Ensemble U))(Included U (Empty_set U) A).
-Proof.
-Intro; Red.
-Intros x H; Elim (Noone_in_empty x); Auto with sets.
-Qed.
-Hints Resolve Included_Empty.
-
-Lemma Add_intro1:
-  (A: (Ensemble U)) (x, y: U) (In U A y) -> (In U (Add U A x) y).
-Proof.
-Unfold 1 Add; Auto with sets.
-Qed.
-Hints Resolve Add_intro1.
-
-Lemma Add_intro2: (A: (Ensemble U)) (x: U) (In U (Add U A x) x).
-Proof.
-Unfold 1 Add; Auto with sets.
-Qed.
-Hints Resolve Add_intro2.
-
-Lemma Inhabited_add: (A: (Ensemble U)) (x: U) (Inhabited U (Add U A x)).
-Proof.
-Intros A x.
-Apply Inhabited_intro with x := x; Auto with sets.
-Qed.
-Hints Resolve Inhabited_add.
-
-Lemma Inhabited_not_empty:
-  (X: (Ensemble U)) (Inhabited U X) -> ~ X == (Empty_set U).
-Proof.
-Intros X H'; Elim H'.
-Intros x H'0; Red; Intro H'1.
-Absurd (In U X x); Auto with sets.
-Rewrite H'1; Auto with sets.
-Qed.
-Hints Resolve Inhabited_not_empty.
-
-Lemma Add_not_Empty :
- (A: (Ensemble U)) (x: U) ~ (Add U A x) == (Empty_set U).
-Proof.
-Auto with sets.
-Qed.
-Hints Resolve Add_not_Empty.
-
-Lemma not_Empty_Add :
- (A: (Ensemble U)) (x: U) ~ (Empty_set U) == (Add U A x).
-Proof.
-Intros; Red; Intro H; Generalize (Add_not_Empty A x); Auto with sets.
-Qed.
-Hints Resolve not_Empty_Add.
-
-Lemma Singleton_inv: (x, y: U) (In U (Singleton U x) y) -> x == y.
-Proof.
-Intros x y H'; Elim H'; Trivial with sets.
-Qed.
-Hints Resolve Singleton_inv.
-
-Lemma Singleton_intro: (x, y: U) x == y -> (In U (Singleton U x) y).
-Proof.
-Intros x y H'; Rewrite H'; Trivial with sets.
-Qed.
-Hints Resolve Singleton_intro.
-
-Lemma Union_inv:  (B, C: (Ensemble U)) (x: U) 
-  (In U (Union U B C) x) -> (In U B x) \/ (In U C x).
-Proof.
-Intros B C x H'; Elim H'; Auto with sets.
-Qed.
-
-Lemma Add_inv:
-  (A: (Ensemble U)) (x, y: U) (In U (Add U A x) y) -> (In U A y) \/ x == y.
-Proof.
-Intros A x y H'; Elim H'; Auto with sets.
-Qed.
-
-Lemma Intersection_inv:
-  (B, C: (Ensemble U)) (x: U) (In U (Intersection U B C) x) ->
-   (In U B x) /\ (In U C x).
-Proof.
-Intros B C x H'; Elim H'; Auto with sets.
-Qed.
-Hints Resolve Intersection_inv.
-
-Lemma Couple_inv: (x, y, z: U) (In U (Couple U x y) z) -> z == x \/ z == y.
-Proof.
-Intros x y z H'; Elim H'; Auto with sets.
-Qed.
-Hints Resolve Couple_inv.
-
-Lemma Setminus_intro:
-  (A, B: (Ensemble U)) (x: U) (In U A x) -> ~ (In U B x) ->
-   (In U (Setminus U A B) x).
-Proof.
-Unfold 1 Setminus; Red; Auto with sets.
-Qed.
-Hints Resolve Setminus_intro.
- 
-Lemma Strict_Included_intro:
-  (X, Y: (Ensemble U)) (Included U X Y) /\ ~ X == Y -> 
-                       (Strict_Included U X Y).
-Proof.
-Auto with sets.
-Qed.
-Hints Resolve Strict_Included_intro.
-
-Lemma Strict_Included_strict: (X: (Ensemble U)) ~ (Strict_Included U X X).
-Proof.
-Intro X; Red; Intro H'; Elim H'.
-Intros H'0 H'1; Elim H'1; Auto with sets.
-Qed.
-Hints Resolve Strict_Included_strict.
-
-End Ensembles_facts.
-
-Hints Resolve Singleton_inv Singleton_intro Add_intro1 Add_intro2 
-	Intersection_inv Couple_inv Setminus_intro Strict_Included_intro
-	Strict_Included_strict Noone_in_empty Inhabited_not_empty
-	Add_not_Empty  not_Empty_Add Inhabited_add Included_Empty : sets v62.