diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index fa8d7b4c..8e78ae4c 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -25,6 +25,7 @@ end
 
 module Bvar = Sidekick_core_logic.Bvar
 module Lit = Lit
+module Proof_step = Proof_step
 module Proof_core = Proof_core
 module Proof_sat = Proof_sat
 module Proof_trace = Proof_trace
diff --git a/src/core/proof_step.ml b/src/core/proof_step.ml
new file mode 100644
index 00000000..f814bcaf
--- /dev/null
+++ b/src/core/proof_step.ml
@@ -0,0 +1,3 @@
+type id = int32
+
+let pp = Fmt.int32
diff --git a/src/core/proof_term.ml b/src/core/proof_term.ml
index d8ec7882..0600a51a 100644
--- a/src/core/proof_term.ml
+++ b/src/core/proof_term.ml
@@ -1,6 +1,6 @@
 open Sidekick_core_logic
 
-type step_id = int32
+type step_id = Proof_step.id
 type lit = Lit.t
 
 type t = {
diff --git a/src/core/proof_term.mli b/src/core/proof_term.mli
index 9b56cb97..81ef09c3 100644
--- a/src/core/proof_term.mli
+++ b/src/core/proof_term.mli
@@ -4,7 +4,7 @@
 
 open Sidekick_core_logic
 
-type step_id = int32
+type step_id = Proof_step.id
 type lit = Lit.t
 
 type t = {
diff --git a/src/core/proof_trace.ml b/src/core/proof_trace.ml
index 50aac799..ea51bf3d 100644
--- a/src/core/proof_trace.ml
+++ b/src/core/proof_trace.ml
@@ -1,5 +1,5 @@
 type lit = Lit.t
-type step_id = int32
+type step_id = Proof_step.id
 type proof_term = Proof_term.t
 
 module Step_vec = struct
diff --git a/src/core/proof_trace.mli b/src/core/proof_trace.mli
index 19cf533e..0a3c563b 100644
--- a/src/core/proof_trace.mli
+++ b/src/core/proof_trace.mli
@@ -10,7 +10,7 @@ open Sidekick_core_logic
 
 type lit = Lit.t
 
-type step_id = Proof_term.step_id
+type step_id = Proof_step.id
 (** Identifier for a tracing step (like a unique ID for a clause previously
     added/proved) *)