Imported Upstream version 8.1~gammaupstream/8.1.gamma

1 files changed, 14 insertions, 11 deletions

diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v
index 2df0317b..9b2f4057 100644
--- a/theories/Relations/Relations.v
+++ b/theories/Relations/Relations.v
@@ -6,23 +6,26 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Relations.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Relations.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 Require Export Relation_Definitions.
 Require Export Relation_Operators.
 Require Export Operators_Properties.
 
 Lemma inverse_image_of_equivalence :
- forall (A B:Set) (f:A -> B) (r:relation B),
-   equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)).
-intros; split; elim H; red in |- *; auto.
-intros _ equiv_trans _ x y z H0 H1; apply equiv_trans with (f y); assumption.
+  forall (A B:Set) (f:A -> B) (r:relation B),
+    equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)).
+Proof.
+  intros; split; elim H; red in |- *; auto.
+  intros _ equiv_trans _ x y z H0 H1; apply equiv_trans with (f y); assumption.
 Qed.
 
 Lemma inverse_image_of_eq :
- forall (A B:Set) (f:A -> B), equivalence A (fun x y:A => f x = f y).
-split; red in |- *;
- [  (* reflexivity *) reflexivity
- |  (* transitivity *) intros; transitivity (f y); assumption
- |  (* symmetry *) intros; symmetry  in |- *; assumption ].
-Qed.
\ No newline at end of file
+  forall (A B:Set) (f:A -> B), equivalence A (fun x y:A => f x = f y).
+Proof.
+  split; red in |- *;
+    [  (* reflexivity *) reflexivity
+      |  (* transitivity *) intros; transitivity (f y); assumption
+      |  (* symmetry *) intros; symmetry  in |- *; assumption ].
+Qed.
+