16 files changed, 64 insertions, 184 deletions

diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index 589159390..c6532d868 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -43,17 +43,7 @@ Definition NZadd := w_op.(znz_add).
 Definition NZsub := w_op.(znz_sub).
 Definition NZmul := w_op.(znz_mul).
 
-Theorem NZeq_equiv : equiv NZ NZeq.
-Proof.
-unfold equiv, reflexive, symmetric, transitive, NZeq; repeat split; intros; auto.
-now transitivity [| y |].
-Qed.
-
-Add Relation NZ NZeq
- reflexivity proved by (proj1 NZeq_equiv)
- symmetry proved by (proj2 (proj2 NZeq_equiv))
- transitivity proved by (proj1 (proj2 NZeq_equiv))
-as NZeq_rel.
+Instance NZeq_equiv : Equivalence NZeq.
 
 Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
 Proof.
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index dfffe9a7f..bd6db10d9 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -48,7 +48,7 @@ Parameter Zopp : Z -> Z.
 (*Notation "- 1" := (Zopp 1) : IntScope.
 Check (-1).*)
 
-Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd.
+Instance Zopp_wd : Proper (Zeq==>Zeq) Zopp.
 
 Notation "- x" := (Zopp x) (at level 35, right associativity) : IntScope.
 Notation "- 1" := (Zopp (NZsucc NZ0)) : IntScope.
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 648cde197..7b3c0ba6e 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -34,13 +34,13 @@ Theorem Zpred_succ : forall n : Z, P (S n) == n.
 Proof NZpred_succ.
 
 Theorem Zeq_refl : forall n : Z, n == n.
-Proof (proj1 NZeq_equiv).
+Proof (@Equivalence_Reflexive _ _ NZeq_equiv).
 
 Theorem Zeq_sym : forall n m : Z, n == m -> m == n.
-Proof (proj2 (proj2 NZeq_equiv)).
+Proof (@Equivalence_Symmetric _ _ NZeq_equiv).
 
 Theorem Zeq_trans : forall n m p : Z, n == m -> m == p -> n == p.
-Proof (proj1 (proj2 NZeq_equiv)).
+Proof (@Equivalence_Transitive _ _ NZeq_equiv).
 
 Theorem Zneq_sym : forall n m : Z, n ~= m -> m ~= n.
 Proof NZneq_sym.
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 0ff896367..7afa1e442 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -28,16 +28,7 @@ Definition NZadd := Zplus.
 Definition NZsub := Zminus.
 Definition NZmul := Zmult.
 
-Theorem NZeq_equiv : equiv Z NZeq.
-Proof.
-exact (@eq_equiv Z).
-Qed.
-
-Add Relation Z NZeq
- reflexivity proved by (proj1 NZeq_equiv)
- symmetry proved by (proj2 (proj2 NZeq_equiv))
- transitivity proved by (proj1 (proj2 NZeq_equiv))
-as NZeq_rel.
+Instance NZeq_equiv : Equivalence NZeq.
 
 Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
 Proof.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 381b9baf6..3eb5238d9 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -125,17 +125,11 @@ stepr ((fst p + snd n) + (fst m + snd m)) in H3 by ring.
 now apply -> add_cancel_r in H3.
 Qed.
 
-Theorem NZeq_equiv : equiv Z Zeq.
+Instance NZeq_equiv : Equivalence Zeq.
 Proof.
-unfold equiv; repeat split; [apply ZE_refl | apply ZE_trans | apply ZE_sym].
+split; [apply ZE_refl | apply ZE_sym | apply ZE_trans].
 Qed.
 
-Add Relation Z Zeq
- reflexivity proved by (proj1 NZeq_equiv)
- symmetry proved by (proj2 (proj2 NZeq_equiv))
- transitivity proved by (proj1 (proj2 NZeq_equiv))
-as NZeq_rel.
-
 Add Morphism (@pair N N) with signature NE ==> NE ==> Zeq as Zpair_wd.
 Proof.
 intros n1 n2 H1 m1 m2 H2; unfold Zeq; simpl; rewrite H1; now rewrite H2.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 030c589ff..3e029d81b 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -45,16 +45,7 @@ Definition NZadd := Z.add.
 Definition NZsub := Z.sub.
 Definition NZmul := Z.mul.
 
-Theorem NZeq_equiv : equiv Z.t Z.eq.
-Proof.
-repeat split; repeat red; intros; auto; congruence.
-Qed.
-
-Add Relation Z.t Z.eq
- reflexivity proved by (proj1 NZeq_equiv)
- symmetry proved by (proj2 (proj2 NZeq_equiv))
- transitivity proved by (proj1 (proj2 NZeq_equiv))
- as NZeq_rel.
+Instance NZeq_equiv : Equivalence Z.eq.
 
 Add Morphism NZsucc with signature Z.eq ==> Z.eq as NZsucc_wd.
 Proof.
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index a9c023856..8499054b5 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -26,18 +26,12 @@ Parameter Inline NZmul : NZ -> NZ -> NZ.
 (* Unary subtraction (opp) is not defined on natural numbers, so we have
    it for integers only *)
 
-Axiom NZeq_equiv : equiv NZ NZeq.
-Add Relation NZ NZeq
- reflexivity proved by (proj1 NZeq_equiv)
- symmetry proved by (proj2 (proj2 NZeq_equiv))
- transitivity proved by (proj1 (proj2 NZeq_equiv))
-as NZeq_rel.
-
-Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
-Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd.
-Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd.
-Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd.
-Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd.
+Instance NZeq_equiv : Equivalence NZeq.
+Instance NZsucc_wd : Proper (NZeq ==> NZeq) NZsucc.
+Instance NZpred_wd : Proper (NZeq ==> NZeq) NZpred.
+Instance NZadd_wd : Proper (NZeq ==> NZeq ==> NZeq) NZadd.
+Instance NZsub_wd : Proper (NZeq ==> NZeq ==> NZeq) NZsub.
+Instance NZmul_wd : Proper (NZeq ==> NZeq ==> NZeq) NZmul.
 
 Delimit Scope NatIntScope with NatInt.
 Open Local Scope NatIntScope.
@@ -54,7 +48,7 @@ Notation "x * y" := (NZmul x y) : NatIntScope.
 Axiom NZpred_succ : forall n : NZ, P (S n) == n.
 
 Axiom NZinduction :
-  forall A : NZ -> Prop, predicate_wd NZeq A ->
+  forall A : NZ -> Prop, Proper (NZeq==>iff) A ->
     A 0 -> (forall n : NZ, A n <-> A (S n)) -> forall n : NZ, A n.
 
 Axiom NZadd_0_l : forall n : NZ, 0 + n == n.
@@ -77,10 +71,10 @@ Parameter Inline NZle : NZ -> NZ -> Prop.
 Parameter Inline NZmin : NZ -> NZ -> NZ.
 Parameter Inline NZmax : NZ -> NZ -> NZ.
 
-Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd.
-Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd.
-Add Morphism NZmin with signature NZeq ==> NZeq ==> NZeq as NZmin_wd.
-Add Morphism NZmax with signature NZeq ==> NZeq ==> NZeq as NZmax_wd.
+Instance NZlt_wd : Proper (NZeq ==> NZeq ==> iff) NZlt.
+Instance NZle_wd : Proper (NZeq ==> NZeq ==> iff) NZle.
+Instance NZmin_wd : Proper (NZeq ==> NZeq ==> NZeq) NZmin.
+Instance NZmax_wd : Proper (NZeq ==> NZeq ==> NZeq) NZmax.
 
 Notation "x < y" := (NZlt x y) : NatIntScope.
 Notation "x <= y" := (NZle x y) : NatIntScope.
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 985466979..7ad38577f 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -27,7 +27,7 @@ Qed.
 
 Declare Left Step NZE_stepl.
 (* The right step lemma is just the transitivity of NZeq *)
-Declare Right Step (proj1 (proj2 NZeq_equiv)).
+Declare Right Step (@Equivalence_Transitive _ _ NZeq_equiv).
 
 Theorem NZsucc_inj : forall n1 n2 : NZ, S n1 == S n2 -> n1 == n2.
 Proof.
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index 60f2aae7d..6a34d0f7b 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -50,18 +50,15 @@ Implicit Arguments recursion [A].
 
 Axiom pred_0 : P 0 == 0.
 
-Axiom recursion_wd : forall (A : Type) (Aeq : relation A),
-  forall a a' : A, Aeq a a' ->
-    forall f f' : N -> A -> A, fun2_eq Neq Aeq Aeq f f' ->
-      forall x x' : N, x == x' ->
-        Aeq (recursion a f x) (recursion a' f' x').
+Instance recursion_wd (A : Type) (Aeq : relation A) :
+ Proper (Aeq ==> (Neq==>Aeq==>Aeq) ==> Neq ==> Aeq) (@recursion A).
 
 Axiom recursion_0 :
   forall (A : Type) (a : A) (f : N -> A -> A), recursion a f 0 = a.
 
 Axiom recursion_succ :
   forall (A : Type) (Aeq : relation A) (a : A) (f : N -> A -> A),
-    Aeq a a -> fun2_wd Neq Aeq Aeq f ->
+    Aeq a a -> Proper (Neq==>Aeq==>Aeq) f ->
       forall n : N, Aeq (recursion a f (S n)) (f n (recursion a f n)).
 
 (*Axiom dep_rec :
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index a0111a082..60b43f0d2 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -46,13 +46,13 @@ Theorem pred_0 : P 0 == 0.
 Proof pred_0.
 
 Theorem Neq_refl : forall n : N, n == n.
-Proof (proj1 NZeq_equiv).
+Proof (@Equivalence_Reflexive _ _ NZeq_equiv).
 
 Theorem Neq_sym : forall n m : N, n == m -> m == n.
-Proof (proj2 (proj2 NZeq_equiv)).
+Proof (@Equivalence_Symmetric _ _ NZeq_equiv).
 
 Theorem Neq_trans : forall n m p : N, n == m -> m == p -> n == p.
-Proof (proj1 (proj2 NZeq_equiv)).
+Proof (@Equivalence_Transitive _ _ NZeq_equiv).
 
 Theorem neq_sym : forall n m : N, n ~= m -> m ~= n.
 Proof NZneq_sym.
@@ -81,10 +81,10 @@ function (by recursion) that maps 0 to false and the successor to true *)
 Definition if_zero (A : Set) (a b : A) (n : N) : A :=
   recursion a (fun _ _ => b) n.
 
-Add Parametric Morphism (A : Set) : (if_zero A) with signature (eq ==> eq ==> Neq ==> eq) as if_zero_wd.
+Instance if_zero_wd (A : Set) : Proper (eq ==> eq ==> Neq ==> eq) (if_zero A).
 Proof.
-intros; unfold if_zero. apply recursion_wd with (Aeq := (@eq A)).
-reflexivity. unfold fun2_eq; now intros. assumption.
+intros; unfold if_zero.
+repeat red; intros. apply recursion_wd; auto. repeat red; auto.
 Qed.
 
 Theorem if_zero_0 : forall (A : Set) (a b : A), if_zero A a b 0 = a.
@@ -95,7 +95,7 @@ Qed.
 Theorem if_zero_succ : forall (A : Set) (a b : A) (n : N), if_zero A a b (S n) = b.
 Proof.
 intros; unfold if_zero.
-now rewrite (@recursion_succ A (@eq A)); [| | unfold fun2_wd; now intros].
+now rewrite (@recursion_succ A (@eq A)).
 Qed.
 
 Implicit Arguments if_zero [A].
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index e18e3b67f..e2a6df1cc 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -109,12 +109,12 @@ recursion
 
 Infix Local "<<" := def_ltb (at level 70, no associativity).
 
-Lemma lt_base_wd : fun_wd Neq (@eq bool) (if_zero false true).
+Lemma lt_base_wd : Proper (Neq==>eq) (if_zero false true).
 unfold fun_wd; intros; now apply if_zero_wd.
 Qed.
 
 Lemma lt_step_wd :
-fun2_wd Neq (fun_eq Neq (@eq bool)) (fun_eq Neq (@eq bool))
+ fun2_wd Neq (fun_eq Neq (@eq bool)) (fun_eq Neq (@eq bool))
   (fun _ f => fun n => recursion false (fun n' _ => f n') n).
 Proof.
 unfold fun2_wd, fun_eq.
diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v
index 5ad343fe0..da48d2fe0 100644
--- a/theories/Numbers/Natural/Abstract/NIso.v
+++ b/theories/Numbers/Natural/Abstract/NIso.v
@@ -51,8 +51,8 @@ Theorem natural_isomorphism_succ :
   forall n : N1, natural_isomorphism (S1 n) == S2 (natural_isomorphism n).
 Proof.
 unfold natural_isomorphism.
-intro n. now rewrite (@NAxiomsMod1.recursion_succ N2 NAxiomsMod2.Neq) ;
-[ | | unfold fun2_wd; intros; apply NBasePropMod2.succ_wd].
+intro n. rewrite (@NAxiomsMod1.recursion_succ N2 NAxiomsMod2.Neq); auto with *.
+repeat red; intros. apply NBasePropMod2.succ_wd; auto.
 Qed.
 
 Theorem hom_nat_iso : homomorphism natural_isomorphism.
diff --git a/theories/Numbers/Natural/Binary/NBinDefs.v b/theories/Numbers/Natural/Binary/NBinDefs.v
index c2c7767d5..c5122ac08 100644
--- a/theories/Numbers/Natural/Binary/NBinDefs.v
+++ b/theories/Numbers/Natural/Binary/NBinDefs.v
@@ -31,14 +31,7 @@ Definition NZadd := Nplus.
 Definition NZsub := Nminus.
 Definition NZmul := Nmult.
 
-Theorem NZeq_equiv : equiv N NZeq.
-Proof (eq_equiv N).
-
-Add Relation N NZeq
- reflexivity proved by (proj1 NZeq_equiv)
- symmetry proved by (proj2 (proj2 NZeq_equiv))
- transitivity proved by (proj1 (proj2 NZeq_equiv))
-as NZeq_rel.
+Instance NZeq_equiv : Equivalence NZeq.
 
 Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
 Proof.
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 8d9e17fb0..38951218d 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -28,14 +28,7 @@ Definition NZadd := plus.
 Definition NZsub := minus.
 Definition NZmul := mult.
 
-Theorem NZeq_equiv : equiv nat NZeq.
-Proof (eq_equiv nat).
-
-Add Relation nat NZeq
- reflexivity proved by (proj1 NZeq_equiv)
- symmetry proved by (proj2 (proj2 NZeq_equiv))
- transitivity proved by (proj1 (proj2 NZeq_equiv))
-as NZeq_rel.
+Instance NZeq_equiv : Equivalence NZeq.
 
 (* If we say "Add Relation nat (@eq nat)" instead of "Add Relation nat NZeq"
 then the theorem generated for succ_wd below is forall x, succ x = succ x,
@@ -189,13 +182,11 @@ Proof.
 reflexivity.
 Qed.
 
-Theorem recursion_wd : forall (A : Type) (Aeq : relation A),
-  forall a a' : A, Aeq a a' ->
-    forall f f' : nat -> A -> A, fun2_eq (@eq nat) Aeq Aeq f f' ->
-      forall n n' : nat, n = n' ->
-        Aeq (recursion a f n) (recursion a' f' n').
+Instance recursion_wd (A : Type) (Aeq : relation A) :
+ Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A).
 Proof.
-unfold fun2_eq; induction n; intros n' Enn'; rewrite <- Enn' in *; simpl; auto.
+intros A Aeq a a' Ha f f' Hf n n' Hn. subst n'.
+induction n; simpl; auto. apply Hf; auto.
 Qed.
 
 Theorem recursion_0 :
@@ -206,10 +197,10 @@ Qed.
 
 Theorem recursion_succ :
   forall (A : Type) (Aeq : relation A) (a : A) (f : nat -> A -> A),
-    Aeq a a -> fun2_wd (@eq nat) Aeq Aeq f ->
+    Aeq a a -> Proper (eq==>Aeq==>Aeq) f ->
       forall n : nat, Aeq (recursion a f (S n)) (f n (recursion a f n)).
 Proof.
-induction n; simpl; auto.
+unfold Proper, respectful in *; induction n; simpl; auto.
 Qed.
 
 End NPeanoAxiomsMod.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 578cb6256..596603b6f 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -39,16 +39,7 @@ Definition NZadd := N.add.
 Definition NZsub := N.sub.
 Definition NZmul := N.mul.
 
-Theorem NZeq_equiv : equiv N.t N.eq.
-Proof.
-repeat split; repeat red; intros; auto; congruence.
-Qed.
-
-Add Relation N.t N.eq
- reflexivity proved by (proj1 NZeq_equiv)
- symmetry proved by (proj2 (proj2 NZeq_equiv))
- transitivity proved by (proj1 (proj2 NZeq_equiv))
- as NZeq_rel.
+Instance NZeq_equiv : Equivalence N.eq.
 
 Add Morphism NZsucc with signature N.eq ==> N.eq as NZsucc_wd.
 Proof.
@@ -297,14 +288,10 @@ Definition recursion (A : Type) (a : A) (f : N.t -> A -> A) (n : N.t) :=
   Nrect (fun _ => A) a (fun n a => f (N.of_N n) a) (N.to_N n).
 Implicit Arguments recursion [A].
 
-Theorem recursion_wd :
-forall (A : Type) (Aeq : relation A),
-  forall a a' : A, Aeq a a' ->
-    forall f f' : N.t -> A -> A, fun2_eq N.eq Aeq Aeq f f' ->
-      forall x x' : N.t, x == x' ->
-        Aeq (recursion a f x) (recursion a' f' x').
+Instance recursion_wd (A : Type) (Aeq : relation A) :
+ Proper (Aeq ==> (N.eq==>Aeq==>Aeq) ==> N.eq ==> Aeq) (@recursion A).
 Proof.
-unfold fun2_wd, N.eq, fun2_eq.
+unfold N.eq.
 intros A Aeq a a' Eaa' f f' Eff' x x' Exx'.
 unfold recursion.
 unfold N.to_N.
@@ -312,7 +299,7 @@ rewrite <- Exx'; clear x' Exx'.
 replace (Zabs_N [x]) with (N_of_nat (Zabs_nat [x])).
 induction (Zabs_nat [x]).
 simpl; auto.
-rewrite N_of_S, 2 Nrect_step; auto.
+rewrite N_of_S, 2 Nrect_step; auto. apply Eff'; auto.
 destruct [x]; simpl; auto.
 change (nat_of_P p) with (nat_of_N (Npos p)); apply N_of_nat_of_N.
 change (nat_of_P p) with (nat_of_N (Npos p)); apply N_of_nat_of_N.
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index 14ea812f3..ddd1c50c3 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -10,7 +10,7 @@
 
 (*i $Id$ i*)
 
-Require Export Setoid.
+Require Export Setoid Morphisms RelationPairs.
 
 Set Implicit Arguments.
 (*
@@ -104,53 +104,43 @@ Variable Ceq : relation C.
 
 (* "wd" stands for "well-defined" *)
 
-Definition fun_wd (f : A -> B) := forall x y : A, Aeq x y -> Beq (f x) (f y).
+Definition fun_wd (f : A -> B) := Proper (Aeq==>Beq) f.
 
-Definition fun2_wd (f : A -> B -> C) :=
-  forall x x' : A, Aeq x x' -> forall y y' : B, Beq y y' -> Ceq (f x y) (f x' y').
+Definition fun2_wd (f : A -> B -> C) := Proper (Aeq==>Beq==>Ceq) f.
 
-Definition fun_eq : relation (A -> B) :=
-  fun f f' => forall x x' : A, Aeq x x' -> Beq (f x) (f' x').
+Definition fun_eq : relation (A -> B) := (Aeq==>Beq)%signature.
 
 (* Note that reflexivity of fun_eq means that every function
 is well-defined w.r.t. Aeq and Beq, i.e.,
 forall x x' : A, Aeq x x' -> Beq (f x) (f x') *)
 
-Definition fun2_eq (f f' : A -> B -> C) :=
-  forall x x' : A, Aeq x x' -> forall y y' : B, Beq y y' -> Ceq (f x y) (f' x' y').
+Definition fun2_eq (f f' : A -> B -> C) := (Aeq==>Beq==>Ceq)%signature f f'.
 
 End ExtensionalProperties.
 
 (* The following definitions instantiate Beq or Ceq to iff; therefore, they
 have to be outside the ExtensionalProperties section *)
 
-Definition predicate_wd (A : Type) (Aeq : relation A) := fun_wd Aeq iff.
+Definition predicate_wd (A : Type) (Aeq : relation A) := Proper (Aeq==>iff).
 
 Definition relation_wd (A B : Type) (Aeq : relation A) (Beq : relation B) :=
-  fun2_wd Aeq Beq iff.
+  Proper (Aeq==>Beq==>iff).
 
 Definition relations_eq (A B : Type) (R1 R2 : A -> B -> Prop) :=
   forall (x : A) (y : B), R1 x y <-> R2 x y.
 
-Theorem relations_eq_equiv :
-  forall (A B : Type), equiv (A -> B -> Prop) (@relations_eq A B).
+Instance relation_eq_equiv A B : Equivalence (@relations_eq A B).
 Proof.
-intros A B; unfold equiv. split; [| split];
-unfold reflexive, symmetric, transitive, relations_eq.
+intros A B; split;
+unfold Reflexive, Symmetric, Transitive, relations_eq.
 reflexivity.
-intros R1 R2 R3 H1 H2 x y; rewrite H1; apply H2.
 now symmetry.
+intros R1 R2 R3 H1 H2 x y; rewrite H1; apply H2.
 Qed.
 
-Add Parametric Relation (A B : Type) : (A -> B -> Prop) (@relations_eq A B)
-  reflexivity proved by (proj1 (relations_eq_equiv A B))
-  symmetry proved by (proj2 (proj2 (relations_eq_equiv A B)))
-  transitivity proved by (proj1 (proj2 (relations_eq_equiv A B)))
-as relations_eq_rel.
-
-Add Parametric Morphism (A : Type) : (@well_founded A) with signature (@relations_eq A A) ==> iff as well_founded_wd.
+Instance well_founded_wd A : Proper (@relations_eq A A ==> iff) (@well_founded A).
 Proof.
-unfold relations_eq, well_founded; intros R1 R2 H;
+unfold relations_eq, well_founded; intros A R1 R2 H.
 split; intros H1 a; induction (H1 a) as [x H2 H3]; constructor;
 intros y H4; apply H3; [now apply <- H | now apply -> H].
 Qed.
@@ -200,37 +190,10 @@ Variables A B : Set.
 Variable Aeq : relation A.
 Variable Beq : relation B.
 
-Hypothesis EA_equiv : equiv A Aeq.
-Hypothesis EB_equiv : equiv B Beq.
+Definition prod_rel : relation (A * B) := (Aeq * Beq)%signature.
 
-Definition prod_rel : relation (A * B) :=
-  fun p1 p2 => Aeq (fst p1) (fst p2) /\ Beq (snd p1) (snd p2).
-
-Lemma prod_rel_refl : reflexive (A * B) prod_rel.
-Proof.
-unfold reflexive, prod_rel.
-destruct x; split; [apply (proj1 EA_equiv) | apply (proj1 EB_equiv)]; simpl.
-Qed.
-
-Lemma prod_rel_sym : symmetric (A * B) prod_rel.
-Proof.
-unfold symmetric, prod_rel.
-destruct x; destruct y;
-split; [apply (proj2 (proj2 EA_equiv)) | apply (proj2 (proj2 EB_equiv))]; simpl in *; tauto.
-Qed.
-
-Lemma prod_rel_trans : transitive (A * B) prod_rel.
-Proof.
-unfold transitive, prod_rel.
-destruct x; destruct y; destruct z; simpl.
-intros; split; [apply (proj1 (proj2 EA_equiv)) with (y := a0) |
-apply (proj1 (proj2 EB_equiv)) with (y := b0)]; tauto.
-Qed.
-
-Theorem prod_rel_equiv : equiv (A * B) prod_rel.
-Proof.
-unfold equiv; split; [exact prod_rel_refl | split; [exact prod_rel_trans | exact prod_rel_sym]].
-Qed.
+Instance prod_rel_equiv `(Equivalence _ Aeq, Equivalence _ Beq) :
+ Equivalence prod_rel.
 
 End RelationOnProduct.
 
@@ -253,15 +216,4 @@ Proof.
 destruct x; destruct y; simpl; split; now intro.
 Qed.*)
 
-Lemma eq_equiv : forall A : Set, equiv A (@eq A).
-Proof.
-intro A; unfold equiv, reflexive, symmetric, transitive.
-repeat split; [exact (@trans_eq A) | exact (@sym_eq A)].
-(* It is interesting how the tactic split proves reflexivity *)
-Qed.
 
-(*Add Relation (fun A : Set => A) LE_Set
- reflexivity proved by (fun A : Set => (proj1 (eq_equiv A)))
- symmetry proved by (fun A : Set => (proj2 (proj2 (eq_equiv A))))
- transitivity proved by (fun A : Set => (proj1 (proj2 (eq_equiv A))))
-as EA_rel.*)