Merge commit 'upstream/8.0pl3+8.1alpha' into 8.0pl3+8.1alpha

1 files changed, 0 insertions, 28 deletions

diff --git a/theories7/Relations/Relations.v b/theories7/Relations/Relations.v
deleted file mode 100755
index 694d0eec..00000000
--- a/theories7/Relations/Relations.v
+++ /dev/null
@@ -1,28 +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: Relations.v,v 1.1.2.1 2004/07/16 19:31:38 herbelin Exp $ i*)
-
-Require Export Relation_Definitions.
-Require Export Relation_Operators.
-Require Export Operators_Properties.
-
-Lemma inverse_image_of_equivalence : (A,B:Set)(f:A->B)
-  (r:(relation B))(equivalence B r)->(equivalence A [x,y:A](r (f x) (f y))).
-Intros; Split; Elim H; Red; Auto.
-Intros _ equiv_trans _ x y z H0 H1; Apply equiv_trans with (f y); Assumption.
-Qed.
-
-Lemma inverse_image_of_eq : (A,B:Set)(f:A->B)
-  (equivalence A [x,y:A](f x)=(f y)).
-Split; Red;
-[ (* reflexivity *)  Reflexivity
-| (* transitivity *) Intros; Transitivity (f y); Assumption
-| (* symmetry *) Intros; Symmetry; Assumption
-].
-Qed.