diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index 951d5844..25e1b4d0 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -17,6 +17,7 @@ module Fmt = CCFormat
 (** {2 Re-exports from core-logic} *)
 
 module Const = Sidekick_core_logic.Const
+module Str_const = Sidekick_core_logic.Str_const
 
 module Term = struct
   include Sidekick_core_logic.Term
@@ -24,10 +25,9 @@ module Term = struct
   include T_printer
   module Tracer = T_tracer
   module Trace_reader = T_trace_reader
+  module Ref = T_ref
 end
 
-module Gensym = Gensym
-
 (** {2 view} *)
 
 module Bool_view = Bool_view
@@ -38,14 +38,20 @@ module Default_cc_view = Default_cc_view
 
 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
-module Proof_term = Proof_term
 module Subst = Sidekick_core_logic.Subst
 module Var = Sidekick_core_logic.Var
 module Box = Box
 module Clause_tracer = Clause_tracer
+module Gensym = Gensym
 
 exception Resource_exhausted
+
+(** {2 Const decoders for traces} *)
+
+let const_decoders =
+  List.flatten
+    [
+      Sidekick_core_logic.T_builtins.const_decoders;
+      T_ref.const_decoders;
+      Box.const_decoders;
+    ]
diff --git a/src/core/clause_tracer.ml b/src/core/clause_tracer.ml
deleted file mode 100644
index dc846105..00000000
--- a/src/core/clause_tracer.ml
+++ /dev/null
@@ -1,31 +0,0 @@
-module Tr = Sidekick_trace
-
-class type t =
-  object
-    method assert_clause : id:int -> Lit.t Iter.t -> Tr.Entry_id.t
-    method delete_clause : id:int -> Lit.t Iter.t -> unit
-    method unsat_clause : id:int -> Tr.Entry_id.t
-    method encode_lit : Lit.t -> Ser_value.t
-  end
-
-class dummy : t =
-  object
-    method assert_clause ~id:_ _ = Tr.Entry_id.dummy
-    method delete_clause ~id:_ _ = ()
-    method unsat_clause ~id:_ = Tr.Entry_id.dummy
-    method encode_lit _ = Ser_value.null
-  end
-
-let dummy : t = new dummy
-let assert_clause (self : #t) ~id c : Tr.Entry_id.t = self#assert_clause ~id c
-
-let assert_clause' (self : #t) ~id c : unit =
-  ignore (self#assert_clause ~id c : Tr.Entry_id.t)
-
-let unsat_clause (self : #t) ~id : Tr.Entry_id.t = self#unsat_clause ~id
-
-let unsat_clause' (self : #t) ~id : unit =
-  ignore (self#unsat_clause ~id : Tr.Entry_id.t)
-
-let delete_clause (self : #t) ~id c = self#delete_clause ~id c
-let encode_lit (self : #t) lit = self#encode_lit lit
diff --git a/src/core/clause_tracer.mli b/src/core/clause_tracer.mli
deleted file mode 100644
index e9f30ebf..00000000
--- a/src/core/clause_tracer.mli
+++ /dev/null
@@ -1,24 +0,0 @@
-(** Tracer for clauses and literals *)
-
-module Tr = Sidekick_trace
-
-(** Tracer for clauses. *)
-class type t =
-  object
-    method assert_clause : id:int -> Lit.t Iter.t -> Tr.Entry_id.t
-    method delete_clause : id:int -> Lit.t Iter.t -> unit
-    method unsat_clause : id:int -> Tr.Entry_id.t
-    method encode_lit : Lit.t -> Ser_value.t
-  end
-
-class dummy : t
-
-val dummy : t
-(** Dummy tracer, recording nothing. *)
-
-val assert_clause : #t -> id:int -> Lit.t Iter.t -> Tr.Entry_id.t
-val assert_clause' : #t -> id:int -> Lit.t Iter.t -> unit
-val delete_clause : #t -> id:int -> Lit.t Iter.t -> unit
-val unsat_clause : #t -> id:int -> Tr.Entry_id.t
-val unsat_clause' : #t -> id:int -> unit
-val encode_lit : #t -> Lit.t -> Ser_value.t
diff --git a/src/core/proof_core.ml b/src/core/proof_core.ml
deleted file mode 100644
index 7ff4b619..00000000
--- a/src/core/proof_core.ml
+++ /dev/null
@@ -1,29 +0,0 @@
-(* FIXME
-   open Proof_trace
-
-   type lit = Lit.t
-*)
-
-type lit = Lit.t
-
-let lemma_cc lits : Proof_term.t = Proof_term.apply_rule ~lits "core.lemma-cc"
-
-let define_term t1 t2 =
-  Proof_term.apply_rule ~terms:[ t1; t2 ] "core.define-term"
-
-let proof_r1 p1 p2 = Proof_term.apply_rule ~premises:[ p1; p2 ] "core.r1"
-let proof_p1 p1 p2 = Proof_term.apply_rule ~premises:[ p1; p2 ] "core.p1"
-
-let proof_res ~pivot p1 p2 =
-  Proof_term.apply_rule ~terms:[ pivot ] ~premises:[ p1; p2 ] "core.res"
-
-let with_defs pr defs =
-  Proof_term.apply_rule ~premises:(pr :: defs) "core.with-defs"
-
-let lemma_true t = Proof_term.apply_rule ~terms:[ t ] "core.true"
-
-let lemma_preprocess t1 t2 ~using =
-  Proof_term.apply_rule ~terms:[ t1; t2 ] ~premises:using "core.preprocess"
-
-let lemma_rw_clause pr ~res ~using =
-  Proof_term.apply_rule ~premises:(pr :: using) ~lits:res "core.rw-clause"
diff --git a/src/core/proof_core.mli b/src/core/proof_core.mli
deleted file mode 100644
index 0a440a06..00000000
--- a/src/core/proof_core.mli
+++ /dev/null
@@ -1,59 +0,0 @@
-(** Core proofs for SMT and congruence closure. *)
-
-open Sidekick_core_logic
-
-type lit = Lit.t
-
-val lemma_cc : lit list -> Proof_term.t
-(** [lemma_cc proof lits] asserts that [lits] form a tautology for the theory
-     of uninterpreted functions. *)
-
-val define_term : Term.t -> Term.t -> Proof_term.t
-(** [define_term cst u proof] defines the new constant [cst] as being equal
-     to [u].
-     The result is a proof of the clause [cst = u] *)
-
-val proof_p1 : Proof_term.step_id -> Proof_term.step_id -> Proof_term.t
-(** [proof_p1 p1 p2], where [p1] proves the unit clause [t=u] (t:bool)
-     and [p2] proves [C \/ t], is the Proof_term.t that produces [C \/ u],
-     i.e unit paramodulation. *)
-
-val proof_r1 : Proof_term.step_id -> Proof_term.step_id -> Proof_term.t
-(** [proof_r1 p1 p2], where [p1] proves the unit clause [|- t] (t:bool)
-       and [p2] proves [C \/ ¬t], is the Proof_term.t that produces [C \/ u],
-       i.e unit resolution. *)
-
-val proof_res :
-  pivot:Term.t -> Proof_term.step_id -> Proof_term.step_id -> Proof_term.t
-(** [proof_res ~pivot p1 p2], where [p1] proves the clause [|- C \/ l]
-     and [p2] proves [D \/ ¬l], where [l] is either [pivot] or [¬pivot],
-     is the Proof_term.t that produces [C \/ D], i.e boolean resolution. *)
-
-val with_defs : Proof_term.step_id -> Proof_term.step_id list -> Proof_term.t
-(** [with_defs pr defs] specifies that [pr] is valid only in
-       a context where the definitions [defs] are present. *)
-
-val lemma_true : Term.t -> Proof_term.t
-(** [lemma_true (true) p] asserts the clause [(true)] *)
-
-val lemma_preprocess :
-  Term.t -> Term.t -> using:Proof_term.step_id list -> Proof_term.t
-(** [lemma_preprocess t u ~using p] asserts that [t = u] is a tautology
-     and that [t] has been preprocessed into [u].
-
-     The theorem [/\_{eqn in using} eqn |- t=u] is proved using congruence
-     closure, and then resolved against the clauses [using] to obtain
-     a unit equality.
-
-     From now on, [t] and [u] will be used interchangeably.
-     @return a Proof_term.t ID for the clause [(t=u)]. *)
-
-val lemma_rw_clause :
-  Proof_term.step_id ->
-  res:lit list ->
-  using:Proof_term.step_id list ->
-  Proof_term.t
-(** [lemma_rw_clause prc ~res ~using], where [prc] is the proof of [|- c],
-     uses the equations [|- p_i = q_i] from [using]
-     to rewrite some literals of [c] into [res]. This is used to preprocess
-     literals of a clause (using {!lemma_preprocess} individually). *)
diff --git a/src/core/proof_sat.ml b/src/core/proof_sat.ml
deleted file mode 100644
index 30733098..00000000
--- a/src/core/proof_sat.ml
+++ /dev/null
@@ -1,10 +0,0 @@
-type lit = Lit.t
-
-let sat_input_clause lits : Proof_term.t =
-  Proof_term.apply_rule "sat.input" ~lits
-
-let sat_redundant_clause lits ~hyps : Proof_term.t =
-  Proof_term.apply_rule "sat.rup" ~lits ~premises:(Iter.to_rev_list hyps)
-
-let sat_unsat_core lits : Proof_term.t =
-  Proof_term.apply_rule ~lits "sat.unsat-core"
diff --git a/src/core/proof_sat.mli b/src/core/proof_sat.mli
deleted file mode 100644
index 7c94a270..00000000
--- a/src/core/proof_sat.mli
+++ /dev/null
@@ -1,15 +0,0 @@
-(** SAT-solver proof emission. *)
-
-open Proof_term
-
-type lit = Lit.t
-
-val sat_input_clause : lit list -> Proof_term.t
-(** Emit an input clause. *)
-
-val sat_redundant_clause : lit list -> hyps:step_id Iter.t -> Proof_term.t
-(** Emit a clause deduced by the SAT solver, redundant wrt previous clauses.
-    The clause must be RUP wrt [hyps]. *)
-
-val sat_unsat_core : lit list -> Proof_term.t
-(** TODO: is this relevant here? *)
diff --git a/src/core/proof_step.ml b/src/core/proof_step.ml
deleted file mode 100644
index f814bcaf..00000000
--- a/src/core/proof_step.ml
+++ /dev/null
@@ -1,3 +0,0 @@
-type id = int32
-
-let pp = Fmt.int32
diff --git a/src/core/proof_term.ml b/src/core/proof_term.ml
deleted file mode 100644
index 2859c0ac..00000000
--- a/src/core/proof_term.ml
+++ /dev/null
@@ -1,44 +0,0 @@
-open Sidekick_core_logic
-
-type step_id = Proof_step.id
-type local_ref = int
-type lit = Lit.t
-
-type rule_apply = {
-  rule_name: string;
-  lit_args: lit list;
-  term_args: Term.t list;
-  subst_args: Subst.t list;
-  premises: step_id list;
-  indices: int list;
-}
-
-type t =
-  | P_ref of step_id
-  | P_local of local_ref
-  | P_let of (local_ref * t) list * t
-  | P_apply of rule_apply
-
-type delayed = unit -> t
-
-let pp out _ = Fmt.string out "<proof term>" (* TODO *)
-
-let local_ref id = P_local id
-let ref_ id = P_ref id
-
-let let_ bs r =
-  match bs with
-  | [] -> r
-  | _ -> P_let (bs, r)
-
-let apply_rule ?(lits = []) ?(terms = []) ?(substs = []) ?(premises = [])
-    ?(indices = []) rule_name : t =
-  P_apply
-    {
-      rule_name;
-      lit_args = lits;
-      subst_args = substs;
-      term_args = terms;
-      premises;
-      indices;
-    }
diff --git a/src/core/proof_term.mli b/src/core/proof_term.mli
deleted file mode 100644
index 85076798..00000000
--- a/src/core/proof_term.mli
+++ /dev/null
@@ -1,41 +0,0 @@
-(** Proof terms.
-
-  A proof term is the description of a reasoning step, that yields a clause. *)
-
-open Sidekick_core_logic
-
-type step_id = Proof_step.id
-type local_ref = int
-type lit = Lit.t
-
-type rule_apply = {
-  rule_name: string;
-  lit_args: lit list;
-  term_args: Term.t list;
-  subst_args: Subst.t list;
-  premises: step_id list;
-  indices: int list;
-}
-
-type t =
-  | P_ref of step_id
-  | P_local of local_ref  (** Local reference, in a let *)
-  | P_let of (local_ref * t) list * t
-  | P_apply of rule_apply
-
-type delayed = unit -> t
-
-include Sidekick_sigs.PRINT with type t := t
-
-val ref_ : step_id -> t
-val local_ref : local_ref -> t
-val let_ : (local_ref * t) list -> t -> t
-
-val apply_rule :
-  ?lits:lit list ->
-  ?terms:Term.t list ->
-  ?substs:Subst.t list ->
-  ?premises:step_id list ->
-  ?indices:int list ->
-  string ->
-  t
diff --git a/src/core/proof_trace.ml b/src/core/proof_trace.ml
deleted file mode 100644
index 39c73263..00000000
--- a/src/core/proof_trace.ml
+++ /dev/null
@@ -1,51 +0,0 @@
-type lit = Lit.t
-type step_id = Proof_step.id
-
-module Step_vec = struct
-  type elt = step_id
-  type t = elt Vec.t
-
-  let get = Vec.get
-  let size = Vec.size
-  let iter = Vec.iter
-  let iteri = Vec.iteri
-  let create ?cap:_ () = Vec.create ()
-  let clear = Vec.clear
-  let copy = Vec.copy
-  let is_empty = Vec.is_empty
-  let push = Vec.push
-  let fast_remove = Vec.fast_remove
-  let filter_in_place = Vec.filter_in_place
-  let ensure_size v len = Vec.ensure_size v ~elt:0l len
-  let pop = Vec.pop_exn
-  let set = Vec.set
-  let shrink = Vec.shrink
-  let to_iter = Vec.to_iter
-end
-
-module type DYN = sig
-  val enabled : unit -> bool
-  val add_step : Proof_term.delayed -> step_id
-  val add_unsat : step_id -> unit
-  val delete : step_id -> unit
-  val close : unit -> unit
-end
-
-type t = (module DYN)
-
-let[@inline] enabled ((module Tr) : t) : bool = Tr.enabled ()
-let[@inline] add_step ((module Tr) : t) rule : step_id = Tr.add_step rule
-let[@inline] add_unsat ((module Tr) : t) s : unit = Tr.add_unsat s
-let[@inline] delete ((module Tr) : t) s : unit = Tr.delete s
-let[@inline] close ((module Tr) : t) : unit = Tr.close ()
-let make (d : (module DYN)) : t = d
-let dummy_step_id : step_id = -1l
-
-let dummy : t =
-  (module struct
-    let enabled () = false
-    let add_step _ = dummy_step_id
-    let add_unsat _ = ()
-    let delete _ = ()
-    let close _ = ()
-  end)
diff --git a/src/core/proof_trace.mli b/src/core/proof_trace.mli
deleted file mode 100644
index b276f1e4..00000000
--- a/src/core/proof_trace.mli
+++ /dev/null
@@ -1,65 +0,0 @@
-(** Proof traces.
-
-    A proof trace is a log of all the deductive reasoning steps made by
-    the SMT solver and other reasoning components. It essentially stores
-    a DAG of all these steps, where each step points (via {!step_id})
-    to its premises.
-*)
-
-type lit = Lit.t
-
-type step_id = Proof_step.id
-(** Identifier for a tracing step (like a unique ID for a clause previously
-    added/proved) *)
-
-module Step_vec : Vec_sig.BASE with type elt = step_id
-(** A vector indexed by steps. *)
-
-(** {2 Traces} *)
-
-type t
-(** The proof trace itself.
-
-    A proof trace is a log of all deductive steps taken by the solver,
-    so we can later reconstruct a certificate for proof-checking.
-
-    Each step in the proof trace should be a {b valid
-    lemma} (of its theory) or a {b valid consequence} of previous steps.
-*)
-
-val enabled : t -> bool
-(** Is proof tracing enabled? *)
-
-val add_step : t -> Proof_term.delayed -> step_id
-(** Create a new step in the trace. *)
-
-val add_unsat : t -> step_id -> unit
-(** Signal "unsat" result at the given proof *)
-
-val delete : t -> step_id -> unit
-(** Forget a step that won't be used in the rest of the trace.
-    Only useful for performance/memory considerations. *)
-
-val close : t -> unit
-(** [close p] closes the proof, and can dispose of underlying resources *)
-
-(** {2 Dummy backend} *)
-
-val dummy_step_id : step_id
-
-val dummy : t
-(** Dummy proof trace, logs nothing. *)
-
-(* TODO: something that just logs on stderr? or uses "Log"? *)
-
-(** {2 Dynamic interface} *)
-
-module type DYN = sig
-  val enabled : unit -> bool
-  val add_step : Proof_term.delayed -> step_id
-  val add_unsat : step_id -> unit
-  val delete : step_id -> unit
-  val close : unit -> unit
-end
-
-val make : (module DYN) -> t
diff --git a/src/core/t_tracer.ml b/src/core/t_tracer.ml
index f712043e..33e4f99e 100644
--- a/src/core/t_tracer.ml
+++ b/src/core/t_tracer.ml
@@ -3,18 +3,6 @@ module Tr = Sidekick_trace
 module T = Term
 
 type term_ref = Tr.entry_id
-
-type Tr.entry_view +=
-  | T_ty of int
-  | T_app of term_ref * term_ref
-  | T_var of string * term_ref
-  | T_bvar of int * term_ref
-  | T_const of { c: Const.view; c_ops: Const.Ops.t; ty: term_ref }
-  | T_lam of { v_name: string; v_ty: term_ref; body: term_ref }
-  | T_pi of { v_name: string; v_ty: term_ref; body: term_ref }
-  (* FIXME: remove when we decode *)
-  [@@ocaml.warning "-38"]
-
 type state = { sink: Tr.Sink.t; emitted: Tr.Entry_id.t T.Weak_map.t }
 
 let emit_term_ (self : state) (t : Term.t) =
diff --git a/src/core/t_tracer.mli b/src/core/t_tracer.mli
index 7e64c75f..c0a038bb 100644
--- a/src/core/t_tracer.mli
+++ b/src/core/t_tracer.mli
@@ -8,19 +8,7 @@
 open Sidekick_core_logic
 module Tr = Sidekick_trace
 
-type term_ref = Tr.entry_id
-
-type Tr.entry_view +=
-  private
-  | T_ty of int
-  | T_app of term_ref * term_ref
-  | T_var of string * term_ref
-  | T_bvar of int * term_ref
-  | T_const of { c: Const.view; c_ops: Const.Ops.t; ty: term_ref }
-  | T_lam of { v_name: string; v_ty: term_ref; body: term_ref }
-  | T_pi of { v_name: string; v_ty: term_ref; body: term_ref }
-  (* FIXME: remove *)
-  [@@ocaml.warning "-38"]
+type term_ref = T_ref.t
 
 class type t =
   object