diff options
Diffstat (limited to 'theories/Relations/Relations.v')
| -rw-r--r-- | theories/Relations/Relations.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v index 9b2f4057..9da30e9b 100644 --- a/theories/Relations/Relations.v +++ b/theories/Relations/Relations.v @@ -6,14 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Relations.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Relations.v 9597 2007-02-06 19:44:05Z herbelin $ 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), + forall (A B:Type) (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. @@ -21,7 +21,7 @@ Proof. Qed. Lemma inverse_image_of_eq : - forall (A B:Set) (f:A -> B), equivalence A (fun x y:A => f x = f y). + forall (A B:Type) (f:A -> B), equivalence A (fun x y:A => f x = f y). Proof. split; red in |- *; [ (* reflexivity *) reflexivity |