(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.3                                 *)
(*                               July 1st 1999                              *)
(*                                                                          *)
(****************************************************************************)
(*                                Relations.v                               *)
(****************************************************************************)
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; Apply equiv_trans with (f y); Assumption.
Save.

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
].
Save.


(* $Id: Relations.v,v 1.5 1999/06/29 07:48:53 loiseleu Exp $ *)
