diff --git a/.vscode/settings.json b/.vscode/settings.json
new file mode 100644
index 00000000..f6db4ecf
--- /dev/null
+++ b/.vscode/settings.json
@@ -0,0 +1,13 @@
+{
+  "coqtop.binPath": "_opam/bin",
+  "coqtop.args": [
+
+    "-I", "_build/install/default/lib",
+    "-Q", "_build/default/theories", "Equations",
+    "-Q", "_build/default/examples", "Equations.Examples",
+    "-Q", "_build/default/test-suite", "Equations.TestSuite"
+  ],
+  "cSpell.enabledFileTypes": {
+    "coq": false
+  }
+}
\ No newline at end of file
diff --git a/Makefile b/Makefile
index 2ab62ba8..404db31d 100644
--- a/Makefile
+++ b/Makefile
@@ -11,7 +11,7 @@ install:
 .PHONY: install
 
 test-suite:
-	dune build -p rocq-equations-tests
+	dune build -p rocq-equations,rocq-equations-examples,rocq-equations-tests
 
 .PHONY: test-suite
 
diff --git a/dune-project b/dune-project
index 2c4b9fbd..0d4f4db7 100644
--- a/dune-project
+++ b/dune-project
@@ -21,7 +21,8 @@
   "logpath:Equations"))
  (depends
    (ocaml (>= 4.10.0))
-   (rocq-prover (>= "9.0~"))
+   (rocq-core (>= "9.0~"))
+   (coq-core (>= "9.0~")) ; For coqc shims for dune 
    (ppx_optcomp :build)
    (ocaml-lsp-server :with-dev-setup)))
 
@@ -29,10 +30,12 @@
  (name rocq-equations-examples)
  (synopsis "Examples")
  (description "Examples of use of Equations")
- (depends rocq-equations))
+ (depends rocq-equations
+  (rocq-stdlib (>= "9.0~"))))
 
 (package
  (name rocq-equations-tests)
  (synopsis "Technical package to run tests")
  (description "Do not install")
- (depends rocq-equations))
+ (depends rocq-equations
+  (rocq-stdlib (>= "9.0~"))))
diff --git a/examples/Basics.v b/examples/Basics.v
index 5c53fe0a..0e6061ba 100644
--- a/examples/Basics.v
+++ b/examples/Basics.v
@@ -24,7 +24,7 @@
 
 #[warnings="-deprecated-library-file-since-8.20"]
 From Stdlib Require Import Program Bvector List Relations.
-From Equations Require Import Equations Signature.
+From Equations.Prop Require Import Equations.
 From Stdlib Require Import Utf8.
 
 Set Keyed Unification.
@@ -103,6 +103,7 @@ Module KAxiom.
       on closed or open terms. *)
 End KAxiom.
 
+
 Module KDec.
   (** However, types enjoying a provable instance of the [K] principle are fine using the [With UIP]
       option. Note that the following definition does *not* reduce according to its single clause
diff --git a/examples/Equations_Tutorial_VeriMag.v b/examples/Equations_Tutorial_VeriMag.v
index f457c6cf..2bb74db4 100644
--- a/examples/Equations_Tutorial_VeriMag.v
+++ b/examples/Equations_Tutorial_VeriMag.v
@@ -413,6 +413,8 @@ Derive Signature for vec.
 Arguments nil {A}.
 Arguments cons {A n}.
 
+Declare Scope vector_scope.
+
 Notation "x :: v" := (cons x v) : vector_scope.
 Notation "[ ]" := nil : vector_scope.
 Notation "[ x ]" := (cons x nil) : vector_scope.
diff --git a/examples/Fin.v b/examples/Fin.v
index ef613f49..558d97bb 100644
--- a/examples/Fin.v
+++ b/examples/Fin.v
@@ -9,6 +9,7 @@
 (** An example development of the [fin] datatype using [equations]. *)
 
 From Stdlib.Program Require Import Basics Combinators.
+From Stdlib Require Import Arith.
 From Equations.Prop Require Import Equations.
 Open Scope equations_scope.
 (** [fin n] is the type of naturals smaller than [n]. *)
diff --git a/examples/STLC.v b/examples/STLC.v
index ec5cb0a3..a561fdb7 100644
--- a/examples/STLC.v
+++ b/examples/STLC.v
@@ -19,6 +19,8 @@ From Equations.Prop Require Import Equations.
 From Stdlib Require Import Lia List Utf8.
 Import ListNotations.
 
+Local Obligation Tactic := CoreTactics.equations_simpl.
+
 Set Keyed Unification.
 
 Derive Signature for le CompareSpec.
@@ -600,6 +602,9 @@ Definition her_type (t : type * term * term) :=
   let u' := fst (fst t) in
    { u : type | u = u' \/ type_subterm u u' }.
 
+
+Import Equations.Prop.Relations Equations.Prop.Subterm. (* For Equations's clos_trans and lexprod definitions *)
+
 #[local] Remove Hints t_step : subterm_relation.
 #[local] Remove Hints Subterm.clos_trans_stepr : subterm_relation.
 
diff --git a/examples/ho_finite_branching.v b/examples/ho_finite_branching.v
index fc810ebc..e09090c8 100644
--- a/examples/ho_finite_branching.v
+++ b/examples/ho_finite_branching.v
@@ -1,8 +1,8 @@
 (** * Higher-order recursion, an example with finite branching trees *)
 
 From Equations.Prop Require Import Equations.
-
-Require Import Examples.Fin.
+From Equations Require Import Examples.Fin.
+Local Obligation Tactic := CoreTactics.equations_simpl.
 
 Inductive ho : Set :=
 | base : nat -> ho
diff --git a/examples/polynomials.v b/examples/polynomials.v
index 2b9f8556..3d57ca75 100644
--- a/examples/polynomials.v
+++ b/examples/polynomials.v
@@ -24,7 +24,9 @@ From Stdlib Require Import ZArith Lia.
 From Stdlib Require Import Psatz.
 From Stdlib Require Import Nat.
 #[warnings="-warn-library-file-stdlib-vector"]
-Require Import Stdlib.Vectors.VectorDef.
+Require Import Stdlib.Vectors.Vector.
+
+Local Obligation Tactic := CoreTactics.equations_simpl.
 
 Set Keyed Unification.
 
@@ -262,7 +264,7 @@ Qed.
     We program [eval p v] where [v] is a valuation in [Z] for all the
     variables in [p : poly _ n]. *)
 
-Equations eval {n} {b} (p : poly b n) (v : Vector.t Z n) : Z :=
+Equations eval {n} {b} (p : poly b n) (v : VectorDef.t Z n) : Z :=
   eval poly_z         nil           := 0%Z;
   eval (poly_c z _)   nil           := z;
   eval (poly_l p)     (cons _ xs)   := eval p xs;
diff --git a/examples/wfrec.v b/examples/wfrec.v
index b4d6233b..62929540 100644
--- a/examples/wfrec.v
+++ b/examples/wfrec.v
@@ -9,7 +9,7 @@
 
 From Equations.Prop Require Import Equations.
 From Stdlib Require Import List Syntax Arith Lia.
-From Stdlib Require Import List.
+Local Obligation Tactic := CoreTactics.equations_simpl.
 Import ListNotations.
 (* end hide *)
 (** * Well-founded recursion
@@ -77,7 +77,7 @@ Proof.
   auto.
 Qed.
 
-Equations ack (m n : nat) : nat by wf (m, n) (Equations.Prop.Subterm.lexprod _ _ lt lt) :=
+Equations ack (m n : nat) : nat by wf (m, n) (lexprod _ _ lt lt) :=
   ack 0 0         := 1;
   ack 0 (S n)     := S (S n);
   ack (S m) 0     := ack m 1;
diff --git a/test-suite/Basics.v b/test-suite/Basics.v
index 5cc48234..b42cb20c 100644
--- a/test-suite/Basics.v
+++ b/test-suite/Basics.v
@@ -6,7 +6,8 @@
 (* GNU Lesser General Public License Version 2.1                      *)
 (**********************************************************************)
 
-From Stdlib Require Import Program List Relations.
+#[warnings="-warn-library-file-stdlib-vector"]
+From Stdlib Require Import Program Vector List Relations.
 From Equations.Prop Require Import Equations.
 
 From Stdlib Require Import Utf8.
diff --git a/test-suite/BasicsDec.v b/test-suite/BasicsDec.v
index 0718fca7..c7b9fa84 100644
--- a/test-suite/BasicsDec.v
+++ b/test-suite/BasicsDec.v
@@ -46,7 +46,7 @@ Print Assumptions well_founded_t_subterm.
 Lemma well_founded_vector_direct_subterm' :
   forall A : Type, EqDec A -> WellFounded (t_subterm A).
 Proof. intros.
-  apply Transitive_Closure.wf_clos_trans.
+  apply Relations.wf_clos_trans.
   intro. simp_sigmas.
   induction a0; constructor; intros;
   simp_sigmas. simpl in *.
diff --git a/test-suite/fin.v b/test-suite/fin.v
index 97b32180..4b1b18a8 100644
--- a/test-suite/fin.v
+++ b/test-suite/fin.v
@@ -1,4 +1,4 @@
-From Stdlib Require Import Program.
+From Stdlib Require Import Program Arith.
 From Equations.Prop Require Import EqDecInstances Equations.
 Import Sigma_Notations.
 Local Open Scope equations_scope.
diff --git a/test-suite/nestedrec.v b/test-suite/nestedrec.v
index 4d4d1774..cd875058 100644
--- a/test-suite/nestedrec.v
+++ b/test-suite/nestedrec.v
@@ -1,5 +1,5 @@
 From Equations.Prop Require Import Equations.
-
+From Stdlib Require Import List.
 
 Inductive term : Set :=
 | Var (n : nat)
diff --git a/test-suite/rec.v b/test-suite/rec.v
index 905293ce..a2f06bba 100644
--- a/test-suite/rec.v
+++ b/test-suite/rec.v
@@ -12,6 +12,8 @@ From Stdlib Require Import List Relations.
 From Stdlib Require Import Arith Wf_nat.
 From Stdlib Require Import Lia.
 
+Local Obligation Tactic := CoreTactics.equations_simpl.
+
 Module RecRel.
   Unset Equations With Funext.
 
diff --git a/test-suite/terms.v b/test-suite/terms.v
index a36887fd..15ae2fa5 100644
--- a/test-suite/terms.v
+++ b/test-suite/terms.v
@@ -1,4 +1,5 @@
 From Equations.Prop Require Import Equations.
+From Stdlib Require Import List.
 
 Inductive term :=
 | Var : nat -> term
diff --git a/theories/HoTT/Classes.v b/theories/HoTT/Classes.v
index 40c82a16..db649a93 100644
--- a/theories/HoTT/Classes.v
+++ b/theories/HoTT/Classes.v
@@ -8,7 +8,7 @@
 
 From Equations Require Import Init CoreTactics.
 Set Warnings "-notation-overridden".
-From Stdlib Require Import HoTT.Basics.Trunc HoTT.HSet.
+From Corelib Require Import HoTT.Basics.Trunc HoTT.HSet.
 From Equations Require Import HoTT.Logic Equations.HoTT.Relation
         Equations.HoTT.Relation_Properties Equations.HoTT.WellFounded.
 
diff --git a/theories/HoTT/DepElim.v b/theories/HoTT/DepElim.v
index b657fad0..004baa40 100644
--- a/theories/HoTT/DepElim.v
+++ b/theories/HoTT/DepElim.v
@@ -10,7 +10,7 @@
 
 Set Warnings "-notation-overridden".
 
-From Stdlib Require Import Program.Tactics.
+From Corelib Require Import Program.Tactics.
 Require Export Equations.Init.
 From Equations Require Import Signature CoreTactics.
 From Equations Require Import HoTT.Logic.
diff --git a/theories/HoTT/EqDec.v b/theories/HoTT/EqDec.v
index 745ce455..baccfaf6 100644
--- a/theories/HoTT/EqDec.v
+++ b/theories/HoTT/EqDec.v
@@ -232,7 +232,7 @@ Definition apd_eq {A} {x y : A} (p : x = y) {z} (q : z = x) :
   transport (@paths A z) p q = q @ p.
 Proof. now destruct p, q. Defined.
 
-From Stdlib Require Import HoTT.Basics.Trunc.
+From Corelib Require Import HoTT.Basics.Trunc.
 
 Lemma hprop_hset {A} (h : IsHProp A) : IsHSet A.
 Proof.
diff --git a/theories/HoTT/FunctionalInduction.v b/theories/HoTT/FunctionalInduction.v
index 353d3695..ef9f493b 100644
--- a/theories/HoTT/FunctionalInduction.v
+++ b/theories/HoTT/FunctionalInduction.v
@@ -9,7 +9,7 @@
 Set Warnings "-notation-overridden".
 From Equations Require Import CoreTactics.
 From Equations Require Import HoTT.Logic Equations.HoTT.Classes Equations.HoTT.EqDec Equations.HoTT.DepElim.
-From Stdlib Require Import HoTT.Spaces.Nat.
+From Corelib Require Import HoTT.Spaces.Nat.
 
 Local Open Scope nat_scope.
 Local Open Scope equations_scope.
diff --git a/theories/HoTT/Logic.v b/theories/HoTT/Logic.v
index fecb33d5..a5ab90bb 100644
--- a/theories/HoTT/Logic.v
+++ b/theories/HoTT/Logic.v
@@ -23,7 +23,7 @@ Register ap as core.identity.congr.
 
 Definition path_inspect {A : Type} (x : A) : { y | paths x y } := (x ; idpath).
 
-From Stdlib Require Import HoTT.Types.Bool.
+From Corelib Require Import HoTT.Types.Bool.
 (* For compatibility with Coq's [induction] *)
 Definition Bool_rect := Bool_ind.
 
diff --git a/theories/HoTT/NoConfusion.v b/theories/HoTT/NoConfusion.v
index 88f6263d..187100b9 100644
--- a/theories/HoTT/NoConfusion.v
+++ b/theories/HoTT/NoConfusion.v
@@ -16,7 +16,7 @@ From Equations Require Import Init Signature.
 From Equations Require Import CoreTactics.
 From Equations Require Import HoTT.Logic Equations.HoTT.Classes Equations.HoTT.EqDec Equations.HoTT.Constants.
 From Equations Require Import HoTT.DepElim Equations.HoTT.Tactics.
-From Stdlib Require Import HoTT.Spaces.List.Core.
+From Corelib Require Import HoTT.Spaces.List.Core.
 
 
 (** Parameterized inductive types just need NoConfusion. *)
diff --git a/theories/HoTT/WellFounded.v b/theories/HoTT/WellFounded.v
index fdc42705..22b02d47 100644
--- a/theories/HoTT/WellFounded.v
+++ b/theories/HoTT/WellFounded.v
@@ -2,7 +2,7 @@ Set Warnings "-notation-overridden".
 From Equations Require Import Init CoreTactics.
 From Equations Require Import HoTT.Logic
         Equations.HoTT.Relation Equations.HoTT.Relation_Properties.
-From Stdlib Require Import HoTT.Basics.Tactics.
+From Corelib Require Import HoTT.Basics.Tactics.
 
 Set Universe Polymorphism.
 Import Sigma_Notations.
diff --git a/theories/Init.v b/theories/Init.v
index d5b1ce60..a74dab8a 100644
--- a/theories/Init.v
+++ b/theories/Init.v
@@ -7,7 +7,6 @@
 (**********************************************************************)
 
 From Corelib Require Import Extraction.
-From Stdlib Require Import Unicode.Utf8_core.
 
 Declare ML Module "rocq-runtime.plugins.ltac".
 Declare ML Module "rocq-equations.plugin".
diff --git a/theories/Prop/Classes.v b/theories/Prop/Classes.v
index 3d935017..bd5ab7ee 100644
--- a/theories/Prop/Classes.v
+++ b/theories/Prop/Classes.v
@@ -7,7 +7,7 @@
 (**********************************************************************)
 
 From Equations Require Import Init CoreTactics.
-From Stdlib Require Import Extraction Relation_Definitions.
+From Corelib Require Import Extraction Relation_Definitions.
 From Equations.Prop Require Import Logic.
 
 (** A class for well foundedness proofs.
diff --git a/theories/Prop/Constants.v b/theories/Prop/Constants.v
index ac4740d1..4e93f4dd 100644
--- a/theories/Prop/Constants.v
+++ b/theories/Prop/Constants.v
@@ -1,6 +1,6 @@
 From Equations Require Import Init.
-From Equations.Prop Require Import Classes EqDec DepElim.
-From Stdlib Require Import Relations.
+From Equations.Prop Require Import Classes EqDec DepElim Relations.
+From Corelib Require Import Relation_Definitions.
 
 (** Naturals *)
 Register Init.Datatypes.O as equations.nat.zero.
@@ -52,7 +52,7 @@ Register Init.Datatypes.pair as equations.product.intro.
 Register Classes.WellFounded as equations.wellfounded.class.
 Register Init.Wf.well_founded as equations.wellfounded.type.
 Register Relations.Relation_Definitions.relation as equations.relation.type.
-Register Relation_Operators.clos_trans as equations.relation.transitive_closure.
+Register Equations.Prop.Relations.clos_trans as equations.relation.transitive_closure.
 
 (* Dependent elimination constants *)
 Register Equations.Prop.DepElim.solution_left as equations.depelim.solution_left.
diff --git a/theories/Prop/DepElim.v b/theories/Prop/DepElim.v
index e350f5da..ee2b8b4b 100644
--- a/theories/Prop/DepElim.v
+++ b/theories/Prop/DepElim.v
@@ -8,7 +8,7 @@
 
 (** Tactics related to (dependent) equality and proof irrelevance. *)
 
-From Stdlib Require Import Program.Tactics.
+From Corelib Require Import Program.Tactics.
 Require Export Equations.Init.
 From Equations Require Import CoreTactics.
 From Equations Require Import Signature.
diff --git a/theories/Prop/Equations.v b/theories/Prop/Equations.v
index ba69a6ee..87ebc2d3 100644
--- a/theories/Prop/Equations.v
+++ b/theories/Prop/Equations.v
@@ -13,7 +13,7 @@ From Equations.Prop Require Import Telescopes.
 
 #[export] Existing Instance wf_tele_measure.
 
-From Stdlib Require Import Program.Tactics.
+From Corelib Require Import Program.Tactics.
 
 (* program_solve_wf launches auto on well-founded and propositional (i.e. in Prop) goals *)
 
diff --git a/theories/Prop/FunctionalExtensionality.v b/theories/Prop/FunctionalExtensionality.v
new file mode 100644
index 00000000..e52b36ee
--- /dev/null
+++ b/theories/Prop/FunctionalExtensionality.v
@@ -0,0 +1,26 @@
+(**********************************************************************)
+(* Equations                                                          *)
+(* Copyright (c) 2009-2020 Matthieu Sozeau <matthieu.sozeau@inria.fr> *)
+(**********************************************************************)
+(* This file is distributed under the terms of the                    *)
+(* GNU Lesser General Public License Version 2.1                      *)
+(**********************************************************************)
+
+From Corelib Require Import Relation_Definitions.
+Set Warnings "-notation-overridden".
+From Equations Require Import Init.
+From Equations.Prop Require Import Logic.
+
+(** The polymorphic equality type used by Equations when working with equality in Type. *)
+
+Section FunExt.
+  Context (A : Type) (B : A -> Type).
+
+  Definition functional_extensionality :=
+    forall (f g : forall x, B x), (forall x, f x = g x) -> f = g.
+
+End FunExt.
+
+Axiom funext : forall A B, functional_extensionality A B.
+
+Ltac extensionality x := eapply funext; intros x.
\ No newline at end of file
diff --git a/theories/Prop/Loader.v b/theories/Prop/Loader.v
index d29d29c6..a29e65ef 100644
--- a/theories/Prop/Loader.v
+++ b/theories/Prop/Loader.v
@@ -8,7 +8,7 @@
 
 (** The set of libraries required to run Equations with all features. *)
 
-From Stdlib Require Import Extraction.
+From Corelib Require Import Extraction.
 
 (** This exports tactics *)
 Declare ML Module "rocq-equations.plugin".
@@ -20,7 +20,7 @@ Require Export Equations.Prop.Classes.
 From Equations.Prop Require Import DepElim Constants.
 Require Export Equations.Prop.EqDec.
 Require Export Equations.Prop.EqDecInstances.
-Require Export Equations.Prop.NoConfusion Equations.Prop.Subterm.
+Require Export Equations.Prop.NoConfusion Equations.Prop.Relations Equations.Prop.Subterm.
 Require Export Equations.Prop.Tactics.
 Require Export Equations.Prop.FunctionalInduction. (* funelim tactic *)
 
diff --git a/theories/Prop/Logic.v b/theories/Prop/Logic.v
index 97665df4..b42a8965 100644
--- a/theories/Prop/Logic.v
+++ b/theories/Prop/Logic.v
@@ -1,7 +1,7 @@
 From Equations Require Import Init.
 From Equations.Prop Require Export SigmaNotations.
 
-From Stdlib Require Import Extraction Relation_Definitions.
+From Corelib Require Import Extraction Relation_Definitions.
 
 (** The regular dependent eliminator of equality *)
 Scheme eq_elim := Induction for eq Sort Type.
diff --git a/theories/Prop/NoConfusion.v b/theories/Prop/NoConfusion.v
index 2613091e..31e55dd2 100644
--- a/theories/Prop/NoConfusion.v
+++ b/theories/Prop/NoConfusion.v
@@ -11,7 +11,7 @@
    on some equation. *)
 
 Set Warnings "-deprecated-since-8.20".   
-From Stdlib Require Import Program.Tactics Bvector List.
+From Corelib Require Import Program.Tactics ListDef.
 Set Warnings "deprecated-since-8.20".
 From Equations Require Import Init Signature.
 From Equations Require Import CoreTactics.
diff --git a/theories/Prop/NoCycle.v b/theories/Prop/NoCycle.v
index 2f2d90ac..69712197 100644
--- a/theories/Prop/NoCycle.v
+++ b/theories/Prop/NoCycle.v
@@ -55,7 +55,7 @@ Proof with trivial.
         + firstorder. }
 Qed.
 
-From Stdlib Require Import CRelationClasses.
+From Corelib Require Import CRelationClasses.
 
 #[export]
 Instance nlt_refl : Reflexive nlt.
diff --git a/theories/Prop/Relations.v b/theories/Prop/Relations.v
new file mode 100644
index 00000000..6ef28f14
--- /dev/null
+++ b/theories/Prop/Relations.v
@@ -0,0 +1,71 @@
+(**********************************************************************)
+(* Equations                                                          *)
+(* Copyright (c) 2009-2020 Matthieu Sozeau <matthieu.sozeau@inria.fr> *)
+(**********************************************************************)
+(* This file is distributed under the terms of the                    *)
+(* GNU Lesser General Public License Version 2.1                      *)
+(**********************************************************************)
+
+From Corelib Require Import Relation_Definitions.
+From Corelib Require Import Init.Wf.
+From Corelib Require Export Program.Wf.
+
+(** Explicitely transparent proofs of well-foundedness of transitive closures and 
+  standard ordering on natural numbers. *)
+
+Inductive clos_trans {A} {R : relation A} (x : A) : A -> Prop :=
+| t_step (y:A) : R x y -> clos_trans x y
+| t_trans (y z:A) : clos_trans x y -> clos_trans y z -> clos_trans x z.
+
+Arguments clos_trans A R x y : clear implicits.
+
+#[export]
+Hint Resolve t_step : relations.
+
+Lemma wf_clos_trans {A R} : well_founded R -> well_founded (clos_trans A R).
+Proof.
+  intros wf x.
+  specialize (wf x).
+  induction wf as [x _ Hcl].
+  constructor. intros y cl.
+  induction cl as [y x hxy|]. eapply Hcl, hxy. 
+  apply IHcl2. apply Hcl. apply cl1.
+Defined.
+
+Implicit Types m n p : nat.
+
+Section Well_founded_Nat.
+
+Variable A : Type.
+
+Variable f : A -> nat.
+Definition ltof (a b:A) := f a < f b.
+Definition gtof (a b:A) := f b > f a.
+
+Lemma lt_le_trans x y z : x < y -> y <= z -> x < z.
+Proof. 
+  induction 2; auto.
+Qed.
+
+Lemma succ_le_mono n m : S n <= S m -> n <= m.
+Proof.
+  change n with (pred (S n)) at 2.
+  change m with (pred (S m)) at 2.
+  induction 1; cbn in *. constructor. destruct m0; auto.
+Qed. 
+  
+Theorem well_founded_ltof : well_founded ltof.
+Proof.
+  assert (H : forall n (a:A), f a < n -> Acc ltof a).
+  { intro n; induction n as [|n IHn].
+    - intros a Ha; absurd (f a < 0); auto. inversion Ha.
+    - intros a Ha. apply Acc_intro. unfold ltof at 1. intros b Hb.
+      apply IHn. apply lt_le_trans with (f a); auto. now apply succ_le_mono. }
+  intros a. apply (H (S (f a))). constructor.
+Defined.
+End Well_founded_Nat.
+
+Lemma lt_wf : well_founded lt.
+Proof.
+  exact (well_founded_ltof nat (fun x => x)).
+Defined.
\ No newline at end of file
diff --git a/theories/Prop/Subterm.v b/theories/Prop/Subterm.v
index 3424f248..2403ec76 100644
--- a/theories/Prop/Subterm.v
+++ b/theories/Prop/Subterm.v
@@ -6,14 +6,13 @@
 (* GNU Lesser General Public License Version 2.1                      *)
 (**********************************************************************)
 
-From Stdlib Require Import Wf_nat Relations.
-From Stdlib Require Import Wellfounded Relation_Definitions.
-From Stdlib Require Import Relation_Operators Lexicographic_Product Wf_nat.
-From Stdlib Require Export Program.Wf FunctionalExtensionality.
+From Corelib Require Import Relation_Definitions.
+From Corelib Require Import Init.Wf.
+From Corelib Require Export Program.Wf.
 
 From Equations Require Import Init Signature.
 From Equations Require Import CoreTactics.
-From Equations.Prop Require Import Classes EqDec DepElim Constants.
+From Equations.Prop Require Import Classes EqDec DepElim Constants Relations FunctionalExtensionality.
 
 Generalizable Variables A R S B.
 
@@ -175,8 +174,11 @@ Hint Extern 0 (MR _ _ _ _) => red : rec_decision.
 #[export]
 Instance lt_wf : WellFounded lt := lt_wf.
 
+Theorem lt_succ_diag_r : forall n, n < S n.
+Proof. constructor. Qed.
+
 #[global]
-Hint Resolve PeanoNat.Nat.lt_succ_diag_r : rec_decision.
+Hint Resolve lt_succ_diag_r : rec_decision.
 
 (** We also add hints for transitive closure, not using [t_trans] but forcing to 
    build the proof by successive applications of the inner relation. *)
@@ -186,7 +188,7 @@ Hint Resolve t_step : subterm_relation.
 
 Lemma clos_trans_stepr A (R : relation A) (x y z : A) :
   R y z -> clos_trans A R x y -> clos_trans A R x z.
-Proof. intros Hyz Hxy. exact (t_trans _ _ x y z Hxy (t_step _ _ _ _ Hyz)). Defined.
+Proof. intros Hyz Hxy. exact (@t_trans _ _ x y z Hxy (@t_step _ _ _ _ Hyz)). Defined.
 
 #[global]
 Hint Resolve clos_trans_stepr : subterm_relation.
@@ -201,7 +203,7 @@ Hint Extern 4 (_ = _) => reflexivity : solve_subterm.
 Hint Extern 10 => eapply_hyp : solve_subterm.
 
 Ltac solve_subterm := intros;
-  apply Transitive_Closure.wf_clos_trans;
+  apply wf_clos_trans;
   red; intros; simp_sigmas; on_last_hyp ltac:(fun H => depind H); constructor;
   intros; simp_sigmas; on_last_hyp ltac:(fun HR => depind HR);
   simplify_dep_elim; try typeclasses eauto with solve_subterm.
@@ -284,8 +286,6 @@ Ltac rec_wf_rel recname x rel :=
 
 (** Define non-dependent lexicographic products *)
 
-#[global] Arguments lexprod [A] [B] _ _.
-
 Section Lexicographic_Product.
 
   Variable A : Type.
diff --git a/theories/Prop/Telescopes.v b/theories/Prop/Telescopes.v
index c595dfa5..ee65f747 100644
--- a/theories/Prop/Telescopes.v
+++ b/theories/Prop/Telescopes.v
@@ -1,5 +1,5 @@
 From Equations.Prop Require Import Loader.
-From Stdlib Require Import FunctionalExtensionality.
+From Equations.Prop Require Import FunctionalExtensionality.
 From Equations.Prop Require Import DepElim.
 From Equations.Prop Require Import Tactics.
 From Equations.Prop Require Import FunctionalInduction.
diff --git a/theories/Type/Classes.v b/theories/Type/Classes.v
index 2eedee00..9d37c420 100644
--- a/theories/Type/Classes.v
+++ b/theories/Type/Classes.v
@@ -6,7 +6,7 @@
 (* GNU Lesser General Public License Version 2.1                      *)
 (**********************************************************************)
 
-From Stdlib Require Import Extraction CRelationClasses.
+From Corelib Require Import Extraction CRelationClasses.
 From Equations Require Import Init CoreTactics.
 Set Warnings "-notation-overridden".
 From Equations.Type Require Import Logic Relation Relation_Properties WellFounded.
diff --git a/theories/Type/Constants.v b/theories/Type/Constants.v
index 049d5cb5..4ee4aeb3 100644
--- a/theories/Type/Constants.v
+++ b/theories/Type/Constants.v
@@ -2,7 +2,7 @@ Set Warnings "-notation-overridden".
 
 From Equations Require Import Init.
 From Equations.Type Require Import Logic DepElim EqDec Classes.
-From Stdlib Require Import CRelationClasses Relations.
+From Corelib Require Import CRelationClasses.
 
 (** Naturals *)
 Register Init.Datatypes.O as equations.nat.zero.
diff --git a/theories/Type/DepElim.v b/theories/Type/DepElim.v
index 6eaa6f67..f9e2aa1c 100644
--- a/theories/Type/DepElim.v
+++ b/theories/Type/DepElim.v
@@ -10,7 +10,7 @@
 
 Set Warnings "-notation-overridden".
 
-From Stdlib Require Import Program.Tactics.
+From Corelib Require Import Program.Tactics.
 Require Export Equations.Init.
 From Equations Require Import Signature CoreTactics.
 From Equations.Type Require Import Logic.
diff --git a/theories/Type/FunctionalExtensionality.v b/theories/Type/FunctionalExtensionality.v
index d67c5f16..b8619741 100644
--- a/theories/Type/FunctionalExtensionality.v
+++ b/theories/Type/FunctionalExtensionality.v
@@ -1,6 +1,6 @@
 Set Warnings "-notation-overridden".
 From Equations Require Import Init.
-From Stdlib Require Import CRelationClasses.
+From Corelib Require Import CRelationClasses.
 From Equations.Type Require Import Logic.
 
 (** The polymorphic equality type used by Equations when working with equality in Type. *)
diff --git a/theories/Type/Loader.v b/theories/Type/Loader.v
index e19b4447..e2a534c4 100644
--- a/theories/Type/Loader.v
+++ b/theories/Type/Loader.v
@@ -8,7 +8,7 @@
 
 (** The set of libraries required to run Equations with all features. *)
 
-From Stdlib Require Import Extraction.
+From Corelib Require Import Extraction.
 
 (** This exports tactics *)
 Declare ML Module "rocq-equations.plugin".
diff --git a/theories/Type/Logic.v b/theories/Type/Logic.v
index 83928fe3..b4845539 100644
--- a/theories/Type/Logic.v
+++ b/theories/Type/Logic.v
@@ -1,5 +1,5 @@
 From Equations Require Import Init.
-From Stdlib Require Import Extraction CRelationClasses.
+From Corelib Require Import Extraction CRelationClasses.
 
 Set Warnings "-notation-overridden".
 
diff --git a/theories/Type/Relation.v b/theories/Type/Relation.v
index f96215e0..409e5908 100644
--- a/theories/Type/Relation.v
+++ b/theories/Type/Relation.v
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 From Equations Require Import Init.
-From Stdlib Require Import Extraction CRelationClasses.
+From Corelib Require Import Extraction CRelationClasses.
 
 Set Warnings "-notation-overridden".
 From Equations.Type Require Import Logic.
diff --git a/theories/Type/Relation_Properties.v b/theories/Type/Relation_Properties.v
index 4e671829..645e74a4 100644
--- a/theories/Type/Relation_Properties.v
+++ b/theories/Type/Relation_Properties.v
@@ -16,7 +16,7 @@
 
 Set Warnings "-notation-overridden".
 
-From Stdlib Require Import CRelationClasses.
+From Corelib Require Import CRelationClasses.
 From Equations Require Import Init.
 From Equations.Type Require Import Logic.
 From Equations.Type Require Import Relation.
diff --git a/theories/Type/WellFounded.v b/theories/Type/WellFounded.v
index 860efeb2..34b2209b 100644
--- a/theories/Type/WellFounded.v
+++ b/theories/Type/WellFounded.v
@@ -1,5 +1,5 @@
 Set Warnings "-notation-overridden".
-From Stdlib Require Import Extraction CRelationClasses.
+From Corelib Require Import Extraction CRelationClasses.
 From Equations Require Import Init CoreTactics.
 From Equations.Type Require Import Logic FunctionalExtensionality Relation Relation_Properties.
 
diff --git a/theories/dune b/theories/dune
index 7ee20c7a..ff23d2ee 100644
--- a/theories/dune
+++ b/theories/dune
@@ -4,8 +4,7 @@
  (package rocq-equations)
  (synopsis "Equations Plugin")
  (plugins rocq-runtime.plugins.extraction rocq-equations.plugin)
- (modules :standard \ IdDec NoCycle)
- (theories Stdlib))
+ (modules :standard \ IdDec NoCycle))
 
 (include_subdirs no)
 (dirs ("Prop" "Type"))
\ No newline at end of file