diff --git a/.nix/rocq-overlays/stdlib-subcomponents/default.nix b/.nix/rocq-overlays/stdlib-subcomponents/default.nix
index 3f9cbe4fa8..595c003d32 100644
--- a/.nix/rocq-overlays/stdlib-subcomponents/default.nix
+++ b/.nix/rocq-overlays/stdlib-subcomponents/default.nix
@@ -11,7 +11,7 @@ let
     "logic" = [ ];
     "relations" = [ "corelib-wrapper" ];
     "program" = [ "corelib-wrapper" "logic" ];
-    "classes" = [ "program" "relations" ];
+    "classes" = [ "program" ];
     "bool" = [ "classes" ];
     "structures" = [ "bool" ];
     "arith-base" = [ "structures" ];
@@ -34,7 +34,7 @@ let
     "classical-logic" = [ "arith" ];
     "sets" = [ "classical-logic" ];
     "vectors" = [ "lists" ];
-    "sorting" = [ "lia" "sets" "vectors" ];
+    "sorting" = [ "lia" "sets" "vectors" "relations" ];
     "orders-ex" = [ "strings" "sorting" ];
     "unicode" = [ ];
     "primitive-int" = [ "unicode" "zarith" ];
@@ -45,7 +45,7 @@ let
     "fmaps-fsets-msets" = [ "orders-ex" "zarith" ];
     "extraction" = [ "primitive-string" "primitive-array" "primitive-floats" ];
     "funind" = [ "arith-base" ];
-    "wellfounded" = [ "lists" ];
+    "wellfounded" = [ "relations" "lists" ];
     "streams" = [ "logic" ];
     "rtauto" = [ "positive" "lists" ];
     "compat" = [ "rtauto" "fmaps-fsets-msets" "funind" "extraction" "reals" "zmod" "wellfounded" "streams" ];
diff --git a/doc/changelog/01-changed/162-deprecate-relations.rst b/doc/changelog/01-changed/162-deprecate-relations.rst
new file mode 100644
index 0000000000..799652f1c2
--- /dev/null
+++ b/doc/changelog/01-changed/162-deprecate-relations.rst
@@ -0,0 +1,6 @@
+- in `Wellfounded`
+
+  + Changed definitions to use `RelationClasses` instead of `Relations`
+    (`#162 <https://github.com/coq/stdlib/pull/162>`_,
+    by Andres Erbsen).
+
diff --git a/doc/changelog/05-deprecated/162-deprecate-relations.rst b/doc/changelog/05-deprecated/162-deprecate-relations.rst
new file mode 100644
index 0000000000..d8f1dcb647
--- /dev/null
+++ b/doc/changelog/05-deprecated/162-deprecate-relations.rst
@@ -0,0 +1,18 @@
+- in `Relation_Definitions`
+
+  + Everything except `relation`, in favor of `RelationClasses`
+    (`#162 <https://github.com/coq/stdlib/pull/162>`_,
+    by Andres Erbsen).
+
+- in `Relations`
+
+  + All uses of `Relations`, adding `RelationClasses` versions
+    (`#162 <https://github.com/coq/stdlib/pull/162>`_,
+    by Andres Erbsen).
+
+- in `Operators_Properties`
+
+  + All uses of `Relation_Definitions`, adding `RelationClasses` versions
+    (`#162 <https://github.com/coq/stdlib/pull/162>`_,
+    by Andres Erbsen).
+
diff --git a/doc/stdlib/depends.dot b/doc/stdlib/depends.dot
index e337a3c568..cb24f09638 100644
--- a/doc/stdlib/depends.dot
+++ b/doc/stdlib/depends.dot
@@ -9,7 +9,8 @@ digraph stdlib_deps {
 	];
 	bool -> classes;
 	classes -> program;
-	classes -> relations;
+	wellfounded -> relations;
+	sorting -> relations;
 	program -> "corelib-wrapper";
 	program -> logic;
 	strings -> arith;
diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v
index 97d95a5f50..43cbdff02e 100644
--- a/theories/Classes/RelationPairs.v
+++ b/theories/Classes/RelationPairs.v
@@ -11,7 +11,8 @@
 (** * Relations over pairs *)
 
 
-From Stdlib Require Import Relations Morphisms.
+From Stdlib Require Import Relation_Definitions (relation).
+From Stdlib Require Import Morphisms.
 (* NB: This should be system-wide someday, but for that we need to
     fix the simpl tactic, since "simpl fst" would be refused for
     the moment.
diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v
index 5c7ef8c9dd..694e0a7799 100644
--- a/theories/Relations/Operators_Properties.v
+++ b/theories/Relations/Operators_Properties.v
@@ -29,8 +29,6 @@ Section Properties.
   Arguments clos_trans [A] R x _.
   Arguments clos_trans_1n [A] R x _.
   Arguments clos_trans_n1 [A] R x _.
-  Arguments inclusion [A] R1 R2.
-  Arguments preorder [A] R.
 
   Variable A : Type.
   Variable R : relation A.
@@ -43,8 +41,18 @@ Section Properties.
 
     (** Correctness of the reflexive-transitive closure operator *)
 
-    Lemma clos_rt_is_preorder : preorder R*.
+    #[export] Instance PreOrder_clos_rt : PreOrder R*.
     Proof.
+      split.
+      - exact (rt_refl A R).
+      - exact (rt_trans A R).
+    Qed.
+
+    #[deprecated(since="9.1", use=PreOrder_clos_rt)]
+    #[warning="-deprecated"]
+    Lemma clos_rt_is_preorder : preorder _ R*.
+    Proof.
+      #[warning="-deprecated"]
       apply Build_preorder.
       - exact (rt_refl A R).
       - exact (rt_trans A R).
@@ -52,13 +60,17 @@ Section Properties.
 
     (** Idempotency of the reflexive-transitive closure operator *)
 
-    Lemma clos_rt_idempotent : inclusion (R*)* R*.
+    #[export] Instance subrelation_clos_rt_idemp : subrelation (R*)* R*.
     Proof.
-      red.
       induction 1 as [x y H|x|x y z H IH H0 IH0]; auto with sets.
       apply rt_trans with y; auto with sets.
     Qed.
 
+    #[deprecated(since="9.1", use=subrelation_clos_rt_idemp)]
+    #[warning="-deprecated"]
+    Lemma clos_rt_idempotent : inclusion _ (R*)* R*.
+    Proof. apply subrelation_clos_rt_idemp. Qed.
+
   End Clos_Refl_Trans.
 
   Section Clos_Refl_Sym_Trans.
@@ -66,33 +78,51 @@ Section Properties.
     (** Reflexive-transitive closure is included in the
         reflexive-symmetric-transitive closure *)
 
-    Lemma clos_rt_clos_rst :
-      inclusion (clos_refl_trans R) (clos_refl_sym_trans R).
+    #[export] Instance subrelation_clos_rt_clos_rst :
+      subrelation (clos_refl_trans R) (clos_refl_sym_trans R).
     Proof.
       red.
       induction 1 as [x y H|x|x y z H IH H0 IH0]; auto with sets.
       apply rst_trans with y; auto with sets.
     Qed.
 
+    #[deprecated(since="9.1", use=subrelation_clos_rt_clos_rst)]
+    #[warning="-deprecated"]
+    Lemma clos_rt_clos_rst :
+      inclusion _ (clos_refl_trans R) (clos_refl_sym_trans R).
+    Proof. apply subrelation_clos_rt_clos_rst. Qed.
+
     (** Reflexive closure is included in the
         reflexive-transitive closure *)
 
-    Lemma clos_r_clos_rt :
-      inclusion (clos_refl R) (clos_refl_trans R).
+    #[export] Instance subrelation_clos_r_clos_rt :
+      subrelation (clos_refl R) (clos_refl_trans R).
     Proof.
       induction 1 as [? ?| ].
       - constructor; auto.
       - constructor 2.
     Qed.
 
-    Lemma clos_t_clos_rt :
-      inclusion (clos_trans R) (clos_refl_trans R).
+    #[deprecated(since="9.1", use=subrelation_clos_r_clos_rt)]
+    #[warning="-deprecated"]
+    Lemma clos_r_clos_rt :
+      inclusion _ (clos_refl R) (clos_refl_trans R).
+    Proof. apply subrelation_clos_r_clos_rt. Qed.
+
+    #[export] Instance subrelation_clos_t_clos_rt :
+      subrelation (clos_trans R) (clos_refl_trans R).
     Proof.
       induction 1 as [? ?| ].
       - constructor. auto.
       - econstructor 3; eassumption.
     Qed.
 
+    #[deprecated(since="9.1", use=subrelation_clos_t_clos_rt)]
+    #[warning="-deprecated"]
+    Lemma clos_t_clos_rt :
+      inclusion _ (clos_trans R) (clos_refl_trans R).
+    Proof. apply subrelation_clos_t_clos_rt. Qed.
+
     Lemma clos_rt_t : forall x y z,
       clos_refl_trans R x y -> clos_trans R y z ->
       clos_trans R x z.
@@ -104,9 +134,19 @@ Section Properties.
 
     (** Correctness of the reflexive-symmetric-transitive closure *)
 
+    #[export] Instance Equivalence_clos_rst_is : Equivalence (clos_refl_sym_trans R).
+    Proof.
+      split.
+      - exact (rst_refl A R).
+      - exact (rst_sym A R).
+      - exact (rst_trans A R).
+    Qed.
+
+    #[deprecated(since="9.1", use=Equivalence_clos_rst_is)]
+    #[warning="-deprecated"]
     Lemma clos_rst_is_equiv : equivalence A (clos_refl_sym_trans R).
     Proof.
-      apply Build_equivalence.
+      split.
       - exact (rst_refl A R).
       - exact (rst_trans A R).
       - exact (rst_sym A R).
@@ -114,8 +154,8 @@ Section Properties.
 
     (** Idempotency of the reflexive-symmetric-transitive closure operator *)
 
-    Lemma clos_rst_idempotent :
-      inclusion (clos_refl_sym_trans (clos_refl_sym_trans R))
+    #[export] Instance subrelation_clos_rst_idemp :
+      subrelation (clos_refl_sym_trans (clos_refl_sym_trans R))
       (clos_refl_sym_trans R).
     Proof.
       red.
@@ -123,6 +163,13 @@ Section Properties.
       apply rst_trans with y; auto with sets.
     Qed.
 
+    #[deprecated(since="9.1", use=subrelation_clos_rst_idemp)]
+    #[warning="-deprecated"]
+    Lemma clos_rst_idempotent :
+      inclusion _ (clos_refl_sym_trans (clos_refl_sym_trans R))
+      (clos_refl_sym_trans R).
+    Proof. apply subrelation_clos_rst_idemp. Qed.
+
   End Clos_Refl_Sym_Trans.
 
   Section Equivalences.
@@ -424,33 +471,57 @@ End Properties.
 
 (* begin hide *)
 (* Compatibility *)
+#[deprecated(since="2009", use=clos_trans_tn1)]
 Notation trans_tn1 := clos_trans_tn1 (only parsing).
+#[deprecated(since="2009", use=clos_tn1_trans)]
 Notation tn1_trans := clos_tn1_trans (only parsing).
+#[deprecated(since="2009", use=clos_trans_tn1_iff)]
 Notation tn1_trans_equiv := clos_trans_tn1_iff (only parsing).
 
+#[deprecated(since="2009", use=clos_trans_t1n)]
 Notation trans_t1n := clos_trans_t1n (only parsing).
+#[deprecated(since="2009", use=clos_t1n_trans)]
 Notation t1n_trans := clos_t1n_trans (only parsing).
+#[deprecated(since="2009", use=clos_trans_t1n_iff)]
 Notation t1n_trans_equiv := clos_trans_t1n_iff (only parsing).
 
+#[deprecated(since="2009", use=clos_rtn1_step)]
 Notation R_rtn1 := clos_rtn1_step (only parsing).
+#[deprecated(since="2009", use=clos_rt_rt1n)]
 Notation trans_rt1n := clos_rt_rt1n (only parsing).
+#[deprecated(since="2009", use=clos_rt1n_rt)]
 Notation rt1n_trans := clos_rt1n_rt (only parsing).
+#[deprecated(since="2009", use=clos_rt_rt1n_iff)]
 Notation rt1n_trans_equiv := clos_rt_rt1n_iff (only parsing).
 
+#[deprecated(since="2009", use=clos_rt1n_step)]
 Notation R_rt1n := clos_rt1n_step (only parsing).
+#[deprecated(since="2009", use=clos_rt_rtn1)]
 Notation trans_rtn1 := clos_rt_rtn1 (only parsing).
+#[deprecated(since="2009", use=clos_rtn1_rt)]
 Notation rtn1_trans := clos_rtn1_rt (only parsing).
+#[deprecated(since="2009", use=clos_rt_rtn1_iff)]
 Notation rtn1_trans_equiv := clos_rt_rtn1_iff (only parsing).
 
+#[deprecated(since="2009", use=clos_rst1n_rst)]
 Notation rts1n_rts := clos_rst1n_rst (only parsing).
+#[deprecated(since="2009", use=clos_rst1n_trans)]
 Notation rts_1n_trans := clos_rst1n_trans (only parsing).
+#[deprecated(since="2009", use=clos_rst1n_sym)]
 Notation rts1n_sym := clos_rst1n_sym (only parsing).
+#[deprecated(since="2009", use=clos_rst_rst1n)]
 Notation rts_rts1n := clos_rst_rst1n (only parsing).
+#[deprecated(since="2009", use=clos_rst_rst1n_iff)]
 Notation rts_rts1n_equiv := clos_rst_rst1n_iff (only parsing).
 
+#[deprecated(since="2009", use=clos_rstn1_rst)]
 Notation rtsn1_rts := clos_rstn1_rst (only parsing).
+#[deprecated(since="2009", use=clos_rstn1_trans)]
 Notation rtsn1_trans := clos_rstn1_trans (only parsing).
+#[deprecated(since="2009", use=clos_rstn1_sym)]
 Notation rtsn1_sym := clos_rstn1_sym (only parsing).
+#[deprecated(since="2009", use=clos_rst_rstn1)]
 Notation rts_rtsn1 := clos_rst_rstn1 (only parsing).
+#[deprecated(since="2009", use=clos_rst_rstn1_iff)]
 Notation rts_rtsn1_equiv := clos_rst_rstn1_iff (only parsing).
 (* end hide *)
diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v
index 20de8e64c1..7d3175573b 100644
--- a/theories/Relations/Relation_Definitions.v
+++ b/theories/Relations/Relation_Definitions.v
@@ -1 +1,57 @@
-From Corelib Require Export Relation_Definitions.
+From Corelib Require Export RelationClasses.
+From Corelib Require Import Relation_Definitions.
+
+Notation relation := relation (only parsing).
+
+#[deprecated(since="9.1", use=Reflexive)]
+Notation reflexive := reflexive (only parsing).
+#[deprecated(since="9.1", use=Transitive)]
+Notation transitive := transitive (only parsing).
+#[deprecated(since="9.1", use=Symmetric)]
+Notation symmetric := symmetric (only parsing).
+#[deprecated(since="9.1", use=Antisymmetric)]
+Notation antisymmetric := antisymmetric (only parsing).
+#[deprecated(since="9.1", use=Equivalence)]
+Notation equiv := equiv (only parsing).
+#[deprecated(since="9.1", use=PreOrder)]
+Notation preorder := preorder (only parsing).
+#[deprecated(since="9.1", use=Build_PreOrder)]
+Notation Build_preorder := Build_preorder (only parsing).
+#[deprecated(since="9.1", use=PreOrder_Reflexive)]
+Notation preord_refl := preord_refl (only parsing).
+#[deprecated(since="9.1", use=PreOrder_Transitive)]
+Notation preord_trans := preord_trans (only parsing).
+#[deprecated(since="9.1", use=PartialOrder)]
+Notation order := order (only parsing).
+#[deprecated(since="9.1", note="Use RelationClasses.PartialOrder")]
+Notation Build_order := Build_order (only parsing).
+#[deprecated(since="9.1", use=partial_order_antisym)]
+Notation ord_antisym := ord_antisym (only parsing).
+#[deprecated(since="9.1", note="Use RelationClasses.PartialOrder")]
+Notation ord_refl := ord_refl (only parsing).
+#[deprecated(since="9.1", note="Use RelationClasses.PartialOrder")]
+Notation ord_trans := ord_trans (only parsing).
+#[deprecated(since="9.1", use=Equivalence)]
+Notation equivalence := equivalence (only parsing).
+#[deprecated(since="9.1", use=Build_Equivalence)]
+Notation Build_equivalence := Build_equivalence (only parsing).
+#[deprecated(since="9.1", use=Equivalence_Reflexive)]
+Notation equiv_refl := equiv_refl (only parsing).
+#[deprecated(since="9.1", use=Equivalence_Transitive)]
+Notation equiv_trans := equiv_trans (only parsing).
+#[deprecated(since="9.1", use=Equivalence_Symmetric)]
+Notation equiv_sym := equiv_sym (only parsing).
+#[deprecated(since="9.1", use=RelationClasses.PER)]
+Notation PER := PER (only parsing).
+#[deprecated(since="9.1", use=RelationClasses.Build_PER)]
+Notation Build_PER := Build_PER (only parsing).
+#[deprecated(since="9.1", use=RelationClasses.PER_Symmetric)]
+Notation per_sym := per_sym (only parsing).
+#[deprecated(since="9.1", use=RelationClasses.PER_Transitive)]
+Notation per_trans := per_trans (only parsing).
+#[deprecated(since="9.1", use=subrelation)]
+Notation inclusion := inclusion (only parsing).
+#[deprecated(since="9.1", use=relation_equivalence)]
+Notation same_relation := same_relation (only parsing).
+#[deprecated(since="9.1", note="If you would like the standard library to keep this definition, please open an issue")]
+Notation commut := commut (only parsing).
diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v
index daf84f2e91..b72a2ffa06 100644
--- a/theories/Relations/Relations.v
+++ b/theories/Relations/Relations.v
@@ -7,11 +7,20 @@
 (*         *     GNU Lesser General Public License Version 2.1          *)
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
-
 From Stdlib Require Export Relation_Definitions.
 From Stdlib Require Export Relation_Operators.
 From Stdlib Require Export Operators_Properties.
+From Stdlib Require Export RelationClasses.
+
+Lemma Equivalence_on [A B] (f:A -> B) (r:relation B) :
+    Equivalence r -> Equivalence (fun x y => r (f x) (f y)).
+Proof. intros []; split; red; eauto. Qed.
+
+Lemma Equivalence_eq_on [A B] (f:A -> B) : Equivalence (fun x y => f x = f y).
+Proof. apply Equivalence_on; exact _. Qed.
 
+#[deprecated(since="9.1", use=Equivalence_on)]
+#[warning="-deprecated"]
 Lemma inverse_image_of_equivalence :
   forall (A B:Type) (f:A -> B) (r:relation B),
     equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)).
@@ -20,6 +29,8 @@ Proof.
   intros _ equiv_trans _ x y z H0 H1; apply equiv_trans with (f y); assumption.
 Qed.
 
+#[deprecated(since="9.1", use=Equivalence_eq_on)]
+#[warning="-deprecated"]
 Lemma inverse_image_of_eq :
   forall (A B:Type) (f:A -> B), equivalence A (fun x y:A => f x = f y).
 Proof.
diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index 1c42f25fe0..b9252a64ec 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -7,6 +7,7 @@
 (*         *     GNU Lesser General Public License Version 2.1          *)
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
+Local Set Warnings "-deprecated".
 
 (** This file is deprecated, for a tree on list, use [Mergesort.v]. *)
 
diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v
index 239da46f14..8813ec7c2f 100644
--- a/theories/Sorting/PermutEq.v
+++ b/theories/Sorting/PermutEq.v
@@ -7,6 +7,7 @@
 (*         *     GNU Lesser General Public License Version 2.1          *)
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
+Local Set Warnings "-deprecated".
 
 From Stdlib Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation.
 
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index 8897d6f5f9..8b7a8ea471 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -7,6 +7,7 @@
 (*         *     GNU Lesser General Public License Version 2.1          *)
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
+Local Set Warnings "-deprecated".
 
 From Stdlib Require Import Lia Relations Multiset SetoidList.
 
diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v
index 9f4c17108c..f2b45f3bfc 100644
--- a/theories/Sorting/Sorted.v
+++ b/theories/Sorting/Sorted.v
@@ -20,7 +20,7 @@
   The two notions are equivalent if the order is transitive.
 *)
 
-From Stdlib Require Import List Relations Relations_1.
+From Stdlib Require Import List Relation_Definitions Relations_1.
 
 (* Set Universe Polymorphism. *)
 
diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v
index efdedf86da..7384e77587 100644
--- a/theories/Structures/Orders.v
+++ b/theories/Structures/Orders.v
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-From Stdlib Require Export Relations Morphisms Setoid Equalities.
+From Stdlib Require Export Morphisms Setoid Equalities.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v
index e565dde47d..8fdf84b151 100644
--- a/theories/Wellfounded/Inclusion.v
+++ b/theories/Wellfounded/Inclusion.v
@@ -11,12 +11,13 @@
 (** Author: Bruno Barras *)
 
 From Stdlib Require Import Relation_Definitions.
+From Stdlib Require Import RelationClasses.
 
 Section WfInclusion.
   Variable A : Type.
   Variables R1 R2 : A -> A -> Prop.
 
-  Lemma Acc_incl : inclusion A R1 R2 -> forall z:A, Acc R2 z -> Acc R1 z.
+  Lemma Acc_incl : subrelation R1 R2 -> forall z:A, Acc R2 z -> Acc R1 z.
   Proof.
     induction 2.
     apply Acc_intro; auto with sets.
@@ -25,7 +26,7 @@ Section WfInclusion.
   #[local]
   Hint Resolve Acc_incl : core.
 
-  Theorem wf_incl : inclusion A R1 R2 -> well_founded R2 -> well_founded R1.
+  Theorem wf_incl : subrelation R1 R2 -> well_founded R2 -> well_founded R1.
   Proof.
     unfold well_founded; auto with sets.
   Qed.
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v
index 43336844d7..1d5c6132f9 100644
--- a/theories/Wellfounded/Lexicographic_Exponentiation.v
+++ b/theories/Wellfounded/Lexicographic_Exponentiation.v
@@ -94,7 +94,7 @@ Section Wf_Lexicographic_Exponentiation.
       apply Forall_app. split; [easy|].
       constructor; [|easy].
       eapply rt_trans.
-      + apply clos_r_clos_rt. eassumption.
+      + apply subrelation_clos_r_clos_rt. eassumption.
       + apply Forall_app in IH as [_ IH].
         destruct l as [|? l].
         * now apply rt_refl.
@@ -204,7 +204,7 @@ Section Wf_Lexicographic_Exponentiation.
           intros. eapply clos_rt_t; [|apply t_step]; eassumption. }
         rewrite <-(app_nil_r (a :: l1)).
         apply (clos_trans_list_ext_app_l _ _ _ _ [b]); [assumption|].
-        destruct l2; [apply rt_refl|apply clos_t_clos_rt].
+        destruct l2; [apply rt_refl|apply subrelation_clos_t_clos_rt].
         now apply clos_trans_list_ext_nil_l.
       + apply (dist_Desc_concat [a]) in Hl1 as [_ ?].
         apply (dist_Desc_concat [a]) in Hl2 as [_ ?].
diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v
index eafd07712a..e365510cee 100644
--- a/theories/Wellfounded/Transitive_Closure.v
+++ b/theories/Wellfounded/Transitive_Closure.v
@@ -19,7 +19,7 @@ Section Wf_Transitive_Closure.
 
   Notation trans_clos := (clos_trans A R).
 
-  Lemma incl_clos_trans : inclusion A R trans_clos.
+  Lemma incl_clos_trans : subrelation R trans_clos.
     red; auto with sets.
   Qed.
 
diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v
index 4c9ecc213d..d10eace03e 100644
--- a/theories/Wellfounded/Union.v
+++ b/theories/Wellfounded/Union.v
@@ -20,13 +20,16 @@ Section WfUnion.
 
   Notation Union := (union A R1 R2).
 
+  Local Definition commut (R1 R2:relation A) : Prop :=
+    forall x y:A, R1 y x -> forall z:A, R2 z y ->  exists2 y' : A, R2 y' x & R1 z y'.
+  Context (H : commut R1 R2).
+
   Remark strip_commut :
-    commut A R1 R2 ->
     forall x y:A,
       clos_trans A R1 y x ->
       forall z:A, R2 z y ->  exists2 y' : A, R2 y' x & clos_trans A R1 z y'.
   Proof.
-    induction 2 as [x y| x y z H0 IH1 H1 IH2]; intros.
+    induction 1 as [x y| x y z H0 IH1 H1 IH2]; intros.
     - elim H with y x z; auto with sets; intros x0 H2 H3.
       exists x0; auto with sets.
 
@@ -38,10 +41,9 @@ Section WfUnion.
 
 
   Lemma Acc_union :
-    commut A R1 R2 ->
     (forall x:A, Acc R2 x -> Acc R1 x) -> forall a:A, Acc R2 a -> Acc Union a.
   Proof.
-    induction 3 as [x H1 H2].
+    induction 2 as [x H1 H2].
     apply Acc_intro; intros.
     elim H3; intros; auto with sets.
     cut (clos_trans A R1 y x); auto with sets.
@@ -65,7 +67,7 @@ Section WfUnion.
 
 
   Theorem wf_union :
-    commut A R1 R2 -> well_founded R1 -> well_founded R2 -> well_founded Union.
+    well_founded R1 -> well_founded R2 -> well_founded Union.
   Proof.
     unfold well_founded.
     intros.