diff --git a/src/simplify/dune b/src/simplify/dune
index fa4a9b50..fc9cfc64 100644
--- a/src/simplify/dune
+++ b/src/simplify/dune
@@ -2,5 +2,5 @@
  (name Sidekick_simplify)
  (public_name sidekick.simplify)
  (synopsis "Simplifier")
- (libraries containers iter sidekick.core sidekick.util)
+ (libraries containers iter sidekick.core sidekick.util sidekick.proof)
  (flags :standard -w +32 -open Sidekick_util))
diff --git a/src/simplify/sidekick_simplify.ml b/src/simplify/sidekick_simplify.ml
index c2abd434..ccd11914 100644
--- a/src/simplify/sidekick_simplify.ml
+++ b/src/simplify/sidekick_simplify.ml
@@ -2,17 +2,18 @@ open Sidekick_core
 
 type t = {
   tst: Term.store;
-  proof: Proof_trace.t;
+  proof: Sidekick_proof.Tracer.t;
   mutable hooks: hook list;
   (* store [t --> u by step_ids] in the cache.
      We use a bag for the proof steps because it gives us structural
      sharing of subproofs. *)
-  cache: (Term.t * Proof_step.id Bag.t) Term.Tbl.t;
+  cache: (Term.t * Sidekick_proof.Step.id Bag.t) Term.Tbl.t;
 }
 
-and hook = t -> Term.t -> (Term.t * Proof_step.id Iter.t) option
+and hook = t -> Term.t -> (Term.t * Sidekick_proof.Step.id Iter.t) option
 
 let create tst ~proof : t =
+  let proof = (proof : #Sidekick_proof.Tracer.t :> Sidekick_proof.Tracer.t) in
   { tst; proof; hooks = []; cache = Term.Tbl.create 32 }
 
 let[@inline] tst self = self.tst
@@ -20,7 +21,8 @@ let[@inline] proof self = self.proof
 let add_hook self f = self.hooks <- f :: self.hooks
 let clear self = Term.Tbl.clear self.cache
 
-let normalize (self : t) (t : Term.t) : (Term.t * Proof_step.id) option =
+let normalize (self : t) (t : Term.t) : (Term.t * Sidekick_proof.Step.id) option
+    =
   (* compute and cache normal form of [t] *)
   let rec loop t : Term.t * _ Bag.t =
     match Term.Tbl.find self.cache t with
@@ -67,8 +69,8 @@ let normalize (self : t) (t : Term.t) : (Term.t * Proof_step.id) option =
   else (
     (* proof: [sub_proofs |- t=u] by CC + subproof *)
     let step =
-      Proof_trace.add_step self.proof @@ fun () ->
-      Proof_core.lemma_preprocess t u ~using:(Bag.to_list pr_u)
+      Sidekick_proof.Tracer.add_step self.proof @@ fun () ->
+      Sidekick_proof.Core_rules.lemma_preprocess t u ~using:(Bag.to_list pr_u)
     in
     Some (u, step)
   )
diff --git a/src/simplify/sidekick_simplify.mli b/src/simplify/sidekick_simplify.mli
index 43ee9e54..b25a77ca 100644
--- a/src/simplify/sidekick_simplify.mli
+++ b/src/simplify/sidekick_simplify.mli
@@ -6,16 +6,16 @@ type t
 
 val tst : t -> Term.store
 
-val create : Term.store -> proof:Proof_trace.t -> t
+val create : Term.store -> proof:#Sidekick_proof.Tracer.t -> t
 (** Create a simplifier *)
 
 val clear : t -> unit
 (** Reset internal cache, etc. *)
 
-val proof : t -> Proof_trace.t
+val proof : t -> Sidekick_proof.Tracer.t
 (** Access proof *)
 
-type hook = t -> Term.t -> (Term.t * Proof_step.id Iter.t) option
+type hook = t -> Term.t -> (Term.t * Sidekick_proof.Step.id Iter.t) option
 (** Given a Term.t, try to simplify it. Return [None] if it didn't change.
 
     A simple example could be a hook that takes a Term.t [t],
@@ -28,12 +28,12 @@ type hook = t -> Term.t -> (Term.t * Proof_step.id Iter.t) option
 
 val add_hook : t -> hook -> unit
 
-val normalize : t -> Term.t -> (Term.t * Proof_step.id) option
+val normalize : t -> Term.t -> (Term.t * Sidekick_proof.Step.id) option
 (** Normalize a Term.t using all the hooks. This performs
     a fixpoint, i.e. it only stops when no hook applies anywhere inside
     the Term.t. *)
 
-val normalize_t : t -> Term.t -> Term.t * Proof_step.id option
+val normalize_t : t -> Term.t -> Term.t * Sidekick_proof.Step.id option
 (** Normalize a Term.t using all the hooks, along with a proof that the
     simplification is correct.
     returns [t, ø] if no simplification occurred. *)