1 files changed, 0 insertions, 151 deletions
diff --git a/theories7/Sets/Relations_2_facts.v b/theories7/Sets/Relations_2_facts.v
deleted file mode 100755
index b82438eb..00000000
--- a/theories7/Sets/Relations_2_facts.v
+++ /dev/null
@@ -1,151 +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: Relations_2_facts.v,v 1.1.2.1 2004/07/16 19:31:40 herbelin Exp $ i*)
-
-Require Export Relations_1.
-Require Export Relations_1_facts.
-Require Export Relations_2.
-
-Theorem Rstar_reflexive : 
-  (U: Type) (R: (Relation U)) (Reflexive U (Rstar U R)).
-Proof.
-Auto with sets.
-Qed.
-
-Theorem Rplus_contains_R :
-  (U: Type) (R: (Relation U)) (contains U (Rplus U R) R).
-Proof.
-Auto with sets.
-Qed.
-
-Theorem Rstar_contains_R :
-  (U: Type) (R: (Relation U)) (contains U (Rstar U R) R).
-Proof.
-Intros U R; Red; Intros x y H'; Apply Rstar_n with y; Auto with sets.
-Qed.
-
-Theorem Rstar_contains_Rplus :
-  (U: Type) (R: (Relation U)) (contains U (Rstar U R) (Rplus U R)).
-Proof.
-Intros U R; Red.
-Intros x y H'; Elim H'.
-Generalize Rstar_contains_R; Intro T; Red in T; Auto with sets.
-Intros x0 y0 z H'0 H'1 H'2; Apply Rstar_n with y0; Auto with sets.
-Qed.
-
-Theorem Rstar_transitive :
-  (U: Type) (R: (Relation U)) (Transitive U (Rstar U R)).
-Proof.
-Intros U R; Red.
-Intros x y z H'; Elim H'; Auto with sets.
-Intros x0 y0 z0 H'0 H'1 H'2 H'3; Apply Rstar_n with y0; Auto with sets.
-Qed.
-
-Theorem Rstar_cases :
-  (U: Type) (R: (Relation U)) (x, y: U) (Rstar U R x y) ->
-    x == y \/ (EXT u | (R x u) /\ (Rstar U R u y)).
-Proof.
-Intros U R x y H'; Elim H'; Auto with sets.
-Intros x0 y0 z H'0 H'1 H'2; Right; Exists y0; Auto with sets.
-Qed.
-
-Theorem Rstar_equiv_Rstar1 :
-  (U: Type) (R: (Relation U)) (same_relation U (Rstar U R) (Rstar1 U R)).
-Proof.
-Generalize Rstar_contains_R; Intro T; Red in T.
-Intros U R; Unfold same_relation contains.
-Split; Intros x y H'; Elim H'; Auto with sets.
-Generalize Rstar_transitive; Intro T1; Red in T1.
-Intros x0 y0 z H'0 H'1 H'2 H'3; Apply T1 with y0; Auto with sets.
-Intros x0 y0 z H'0 H'1 H'2; Apply Rstar1_n with y0; Auto with sets.
-Qed.
-
-Theorem Rsym_imp_Rstarsym :
-  (U: Type) (R: (Relation U)) (Symmetric U R) -> (Symmetric U (Rstar U R)).
-Proof.
-Intros U R H'; Red.
-Intros x y H'0; Elim H'0; Auto with sets.
-Intros x0 y0 z H'1 H'2 H'3.
-Generalize Rstar_transitive; Intro T1; Red in T1.
-Apply T1 with y0; Auto with sets.
-Apply Rstar_n with x0; Auto with sets.
-Qed.
-
-Theorem Sstar_contains_Rstar :
-  (U: Type) (R, S: (Relation U)) (contains U (Rstar U S) R) ->
-   (contains U (Rstar U S) (Rstar U R)).
-Proof.
-Unfold contains.
-Intros U R S H' x y H'0; Elim H'0; Auto with sets.
-Generalize Rstar_transitive; Intro T1; Red in T1.
-Intros x0 y0 z H'1 H'2 H'3; Apply T1 with y0; Auto with sets.
-Qed.
-
-Theorem star_monotone :
-  (U: Type) (R, S: (Relation U)) (contains U S R) ->
-   (contains U (Rstar U S) (Rstar U R)).
-Proof.
-Intros U R S H'.
-Apply Sstar_contains_Rstar; Auto with sets.
-Generalize (Rstar_contains_R U S); Auto with sets.
-Qed.
-
-Theorem RstarRplus_RRstar :
-  (U: Type) (R: (Relation U)) (x, y, z: U) 
-    (Rstar U R x y) -> (Rplus U R y z) ->
-    (EXT u | (R x u) /\ (Rstar U R u z)).
-Proof.
-Generalize Rstar_contains_Rplus; Intro T; Red in T.
-Generalize Rstar_transitive; Intro T1; Red in T1.
-Intros U R x y z H'; Elim H'.
-Intros x0 H'0; Elim H'0.
-Intros x1 y0 H'1; Exists y0; Auto with sets.
-Intros x1 y0 z0 H'1 H'2 H'3; Exists y0; Auto with sets.
-Intros x0 y0 z0 H'0 H'1 H'2 H'3; Exists y0.
-Split; [Try Assumption | Idtac].
-Apply T1 with z0; Auto with sets.
-Qed.
-
-Theorem Lemma1 : 
-  (U: Type) (R: (Relation U)) (Strongly_confluent U R) ->
-   (x, b: U) (Rstar U R x b) ->
-    (a: U) (R x a) -> (EXT z | (Rstar U R a z) /\ (R b z)).
-Proof.
-Intros U R H' x b H'0; Elim H'0.
-Intros x0 a H'1; Exists a; Auto with sets.
-Intros x0 y z H'1 H'2 H'3 a H'4.
-Red in H'.
-Specialize 3 H' with x := x0 a := a b := y; Intro H'7; LApply H'7;
- [Intro H'8; LApply H'8;
-   [Intro H'9; Try Exact H'9; Clear H'8 H'7 | Clear H'8 H'7] | Clear H'7]; Auto with sets.
-Elim H'9.
-Intros t H'5; Elim H'5; Intros H'6 H'7; Try Exact H'6; Clear H'5.
-Elim (H'3 t); Auto with sets.
-Intros z1 H'5; Elim H'5; Intros H'8 H'10; Try Exact H'8; Clear H'5.
-Exists z1; Split; [Idtac | Assumption].
-Apply Rstar_n with t; Auto with sets.
-Qed.