diff --git a/src/sigs/cc/dune b/src/sigs/cc/dune
deleted file mode 100644
index a980964b..00000000
--- a/src/sigs/cc/dune
+++ /dev/null
@@ -1,9 +0,0 @@
-
-(library
- (name sidekick_sigs_cc)
- (public_name sidekick.sigs.cc)
- (synopsis "Signatures for the congruence closure")
- (flags :standard -open Sidekick_util)
- (libraries containers iter sidekick.sigs sidekick.sigs.term
-   sidekick.sigs.lit sidekick.sigs.proof-trace sidekick.sigs.proof.core
-   sidekick.util))
diff --git a/src/sigs/cc/sidekick_sigs_cc.ml b/src/sigs/cc/sidekick_sigs_cc.ml
deleted file mode 100644
index 3bb47ec7..00000000
--- a/src/sigs/cc/sidekick_sigs_cc.ml
+++ /dev/null
@@ -1,515 +0,0 @@
-(** Main types for congruence closure *)
-
-module View = View
-
-module type TERM = Sidekick_sigs_term.S
-module type LIT = Sidekick_sigs_lit.S
-module type PROOF_TRACE = Sidekick_sigs_proof_trace.S
-
-(** Arguments to a congruence closure's implementation *)
-module type ARG = sig
-  module T : TERM
-  module Lit : LIT with module T = T
-  module Proof_trace : PROOF_TRACE
-
-  (** Arguments for the congruence closure *)
-  val view_as_cc : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) View.t
-  (** View the term through the lens of the congruence closure *)
-
-  val mk_lit_eq : ?sign:bool -> T.Term.store -> T.Term.t -> T.Term.t -> Lit.t
-  (** [mk_lit_eq store t u] makes the literal [t=u] *)
-
-  module Rule_core :
-    Sidekick_sigs_proof_core.S
-      with type term = T.Term.t
-       and type lit = Lit.t
-       and type step_id = Proof_trace.A.step_id
-       and type rule = Proof_trace.A.rule
-end
-
-(** Collection of input types, and types defined by the congruence closure *)
-module type ARGS_CLASSES_EXPL_EVENT = sig
-  module T : TERM
-  module Lit : LIT with module T = T
-  module Proof_trace : PROOF_TRACE
-
-  type term_store = T.Term.store
-  type term = T.Term.t
-  type value = term
-  type fun_ = T.Fun.t
-  type lit = Lit.t
-  type proof_trace = Proof_trace.t
-  type step_id = Proof_trace.A.step_id
-
-  (** E-node.
-
-      An e-node is a node in the congruence closure that is contained
-      in some equivalence classe).
-      An equivalence class is a set of terms that are currently equal
-      in the partial model built by the solver.
-      The class is represented by a collection of nodes, one of which is
-      distinguished and is called the "representative".
-
-      All information pertaining to the whole equivalence class is stored
-      in its representative's {!E_node.t}.
-
-      When two classes become equal (are "merged"), one of the two
-      representatives is picked as the representative of the new class.
-      The new class contains the union of the two old classes' nodes.
-
-      We also allow theories to store additional information in the
-      representative. This information can be used when two classes are
-      merged, to detect conflicts and solve equations à la Shostak.
-  *)
-  module E_node : sig
-    type t
-    (** An E-node.
-
-        A value of type [t] points to a particular term, but see
-        {!find} to get the representative of the class. *)
-
-    include Sidekick_sigs.PRINT with type t := t
-
-    val term : t -> term
-    (** Term contained in this equivalence class.
-        If [is_root n], then [term n] is the class' representative term. *)
-
-    val equal : t -> t -> bool
-    (** Are two classes {b physically} equal? To check for
-        logical equality, use [CC.E_node.equal (CC.find cc n1) (CC.find cc n2)]
-        which checks for equality of representatives. *)
-
-    val hash : t -> int
-    (** An opaque hash of this E_node.t. *)
-
-    val is_root : t -> bool
-    (** Is the E_node.t a root (ie the representative of its class)?
-        See {!find} to get the root. *)
-
-    val iter_class : t -> t Iter.t
-    (** Traverse the congruence class.
-        Precondition: [is_root n] (see {!find} below) *)
-
-    val iter_parents : t -> t Iter.t
-    (** Traverse the parents of the class.
-        Precondition: [is_root n] (see {!find} below) *)
-
-    (* FIXME:
-       [@@alert refactor "this should be replaced with a Per_class concept"]
-    *)
-
-    type bitfield
-    (** A field in the bitfield of this node. This should only be
-        allocated when a theory is initialized.
-
-        Bitfields are accessed using preallocated keys.
-        See {!CC_S.allocate_bitfield}.
-
-        All fields are initially 0, are backtracked automatically,
-        and are merged automatically when classes are merged. *)
-  end
-
-  (** Explanations
-
-      Explanations are specialized proofs, created by the congruence closure
-      when asked to justify why two terms are equal. *)
-  module Expl : sig
-    type t
-
-    include Sidekick_sigs.PRINT with type t := t
-
-    val mk_merge : E_node.t -> E_node.t -> t
-    (** Explanation: the nodes were explicitly merged *)
-
-    val mk_merge_t : term -> term -> t
-    (** Explanation: the terms were explicitly merged *)
-
-    val mk_lit : lit -> t
-    (** Explanation: we merged [t] and [u] because of literal [t=u],
-        or we merged [t] and [true] because of literal [t],
-        or [t] and [false] because of literal [¬t] *)
-
-    val mk_list : t list -> t
-    (** Conjunction of explanations *)
-
-    val mk_theory : term -> term -> (term * term * t list) list -> step_id -> t
-    (** [mk_theory t u expl_sets pr] builds a theory explanation for
-        why [|- t=u]. It depends on sub-explanations [expl_sets] which
-        are tuples [ (t_i, u_i, expls_i) ] where [expls_i] are
-        explanations that justify [t_i = u_i] in the current congruence closure.
-
-        The proof [pr] is the theory lemma, of the form
-        [ (t_i = u_i)_i |- t=u ].
-        It is resolved against each [expls_i |- t_i=u_i] obtained from
-        [expl_sets], on pivot [t_i=u_i], to obtain a proof of [Gamma |- t=u]
-        where [Gamma] is a subset of the literals asserted into the congruence
-        closure.
-
-        For example for the lemma [a=b] deduced by injectivity
-        from [Some a=Some b] in the theory of datatypes,
-        the arguments would be
-        [a, b, [Some a, Some b, mk_merge_t (Some a)(Some b)], pr]
-        where [pr] is the injectivity lemma [Some a=Some b |- a=b].
-    *)
-  end
-
-  (** Resolved explanations.
-
-      The congruence closure keeps explanations for why terms are in the same
-      class. However these are represented in a compact, cheap form.
-      To use these explanations we need to {b resolve} them into a
-      resolved explanation, typically a list of
-      literals that are true in the current trail and are responsible for
-      merges.
-
-      However, we can also have merged classes because they have the same value
-      in the current model. *)
-  module Resolved_expl : sig
-    type t = { lits: lit list; pr: proof_trace -> step_id }
-
-    include Sidekick_sigs.PRINT with type t := t
-  end
-
-  (** Per-node data *)
-
-  type e_node = E_node.t
-  (** A node of the congruence closure *)
-
-  type repr = E_node.t
-  (** Node that is currently a representative. *)
-
-  type explanation = Expl.t
-end
-
-(** Main congruence closure signature.
-
-    The congruence closure handles the theory QF_UF (uninterpreted
-    function symbols).
-    It is also responsible for {i theory combination}, and provides
-    a general framework for equality reasoning that other
-    theories piggyback on.
-
-    For example, the theory of datatypes relies on the congruence closure
-    to do most of the work, and "only" adds injectivity/disjointness/acyclicity
-    lemmas when needed.
-
-    Similarly, a theory of arrays would hook into the congruence closure and
-    assert (dis)equalities as needed.
-*)
-module type S = sig
-  include ARGS_CLASSES_EXPL_EVENT
-
-  type t
-  (** The congruence closure object.
-      It contains a fair amount of state and is mutable
-      and backtrackable. *)
-
-  (** {3 Accessors} *)
-
-  val term_store : t -> term_store
-  val proof : t -> proof_trace
-
-  val find : t -> e_node -> repr
-  (** Current representative *)
-
-  val add_term : t -> term -> e_node
-  (** Add the term to the congruence closure, if not present already.
-      Will be backtracked. *)
-
-  val mem_term : t -> term -> bool
-  (** Returns [true] if the term is explicitly present in the congruence closure *)
-
-  val allocate_bitfield : t -> descr:string -> E_node.bitfield
-  (** Allocate a new e_node field (see {!E_node.bitfield}).
-
-      This field descriptor is henceforth reserved for all nodes
-      in this congruence closure, and can be set using {!set_bitfield}
-      for each class_ individually.
-      This can be used to efficiently store some metadata on nodes
-      (e.g. "is there a numeric value in the class"
-      or "is there a constructor term in the class").
-
-      There may be restrictions on how many distinct fields are allocated
-      for a given congruence closure (e.g. at most {!Sys.int_size} fields).
-  *)
-
-  val get_bitfield : t -> E_node.bitfield -> E_node.t -> bool
-  (** Access the bit field of the given e_node *)
-
-  val set_bitfield : t -> E_node.bitfield -> bool -> E_node.t -> unit
-  (** Set the bitfield for the e_node. This will be backtracked.
-      See {!E_node.bitfield}. *)
-
-  type propagation_reason = unit -> lit list * step_id
-
-  (** Handler Actions
-
-      Actions that can be scheduled by event handlers. *)
-  module Handler_action : sig
-    type t =
-      | Act_merge of E_node.t * E_node.t * Expl.t
-      | Act_propagate of lit * propagation_reason
-
-    (* TODO:
-       - an action to modify data associated with a class
-    *)
-
-    type conflict = Conflict of Expl.t [@@unboxed]
-
-    type or_conflict = (t list, conflict) result
-    (** Actions or conflict scheduled by an event handler.
-
-      - [Ok acts] is a list of merges and propagations
-      - [Error confl] is a conflict to resolve.
-    *)
-  end
-
-  (** Result Actions.
-
-
-    Actions returned by the congruence closure after calling {!check}. *)
-  module Result_action : sig
-    type t =
-      | Act_propagate of { lit: lit; reason: propagation_reason }
-          (** [propagate (lit, reason)] declares that [reason() => lit]
-          is a tautology.
-
-          - [reason()] should return a list of literals that are currently true,
-            as well as a proof.
-          - [lit] should be a literal of interest (see {!S.set_as_lit}).
-
-          This function might never be called, a congruence closure has the right
-          to not propagate and only trigger conflicts. *)
-
-    type conflict =
-      | Conflict of lit list * step_id
-          (** [raise_conflict (c,pr)] declares that [c] is a tautology of
-          the theory of congruence.
-          @param pr the proof of [c] being a tautology *)
-
-    type or_conflict = (t list, conflict) result
-  end
-
-  (** {3 Events}
-
-      Events triggered by the congruence closure, to which
-      other plugins can subscribe. *)
-
-  (** Events emitted by the congruence closure when something changes. *)
-  val on_pre_merge :
-    t -> (t * E_node.t * E_node.t * Expl.t, Handler_action.or_conflict) Event.t
-  (** [Ev_on_pre_merge acts n1 n2 expl] is emitted right before [n1]
-      and [n2] are merged with explanation [expl].  *)
-
-  val on_pre_merge2 :
-    t -> (t * E_node.t * E_node.t * Expl.t, Handler_action.or_conflict) Event.t
-  (** Second phase of "on pre merge". This runs after {!on_pre_merge}
-      and is used by Plugins. {b NOTE}: Plugin state might be observed as already
-      changed in these handlers. *)
-
-  val on_post_merge :
-    t -> (t * E_node.t * E_node.t, Handler_action.t list) Event.t
-  (** [ev_on_post_merge acts n1 n2] is emitted right after [n1]
-      and [n2] were merged. [find cc n1] and [find cc n2] will return
-      the same E_node.t. *)
-
-  val on_new_term : t -> (t * E_node.t * term, Handler_action.t list) Event.t
-  (** [ev_on_new_term n t] is emitted whenever a new term [t]
-      is added to the congruence closure. Its E_node.t is [n]. *)
-
-  type ev_on_conflict = { cc: t; th: bool; c: lit list }
-  (** Event emitted when a conflict occurs in the CC.
-
-      [th] is true if the explanation for this conflict involves
-      at least one "theory" explanation; i.e. some of the equations
-      participating in the conflict are purely syntactic theories
-      like injectivity of constructors. *)
-
-  val on_conflict : t -> (ev_on_conflict, unit) Event.t
-  (** [ev_on_conflict {th; c}] is emitted when the congruence
-      closure triggers a conflict by asserting the tautology [c]. *)
-
-  val on_propagate :
-    t -> (t * lit * (unit -> lit list * step_id), Handler_action.t list) Event.t
-  (** [ev_on_propagate lit reason] is emitted whenever [reason() => lit]
-      is a propagated lemma. See {!CC_ACTIONS.propagate}. *)
-
-  val on_is_subterm : t -> (t * E_node.t * term, Handler_action.t list) Event.t
-  (** [ev_on_is_subterm n t] is emitted when [n] is a subterm of
-      another E_node.t for the first time. [t] is the term corresponding to
-      the E_node.t [n]. This can be useful for theory combination. *)
-
-  (** {3 Misc} *)
-
-  val n_true : t -> E_node.t
-  (** Node for [true] *)
-
-  val n_false : t -> E_node.t
-  (** Node for [false] *)
-
-  val n_bool : t -> bool -> E_node.t
-  (** Node for either true or false *)
-
-  val set_as_lit : t -> E_node.t -> lit -> unit
-  (** map the given e_node to a literal. *)
-
-  val find_t : t -> term -> repr
-  (** Current representative of the term.
-      @raise E_node.t_found if the term is not already {!add}-ed. *)
-
-  val add_iter : t -> term Iter.t -> unit
-  (** Add a sequence of terms to the congruence closure *)
-
-  val all_classes : t -> repr Iter.t
-  (** All current classes. This is costly, only use if there is no other solution *)
-
-  val explain_eq : t -> E_node.t -> E_node.t -> Resolved_expl.t
-  (** Explain why the two nodes are equal.
-      Fails if they are not, in an unspecified way. *)
-
-  val explain_expl : t -> Expl.t -> Resolved_expl.t
-  (** Transform explanation into an actionable conflict clause *)
-
-  (* FIXME: remove
-        val raise_conflict_from_expl : t -> actions -> Expl.t -> 'a
-        (** Raise a conflict with the given explanation.
-            It must be a theory tautology that [expl ==> absurd].
-            To be used in theories.
-
-            This fails in an unspecified way if the explanation, once resolved,
-            satisfies {!Resolved_expl.is_semantic}. *)
-  *)
-
-  val merge : t -> E_node.t -> E_node.t -> Expl.t -> unit
-  (** Merge these two nodes given this explanation.
-         It must be a theory tautology that [expl ==> n1 = n2].
-         To be used in theories. *)
-
-  val merge_t : t -> term -> term -> Expl.t -> unit
-  (** Shortcut for adding + merging *)
-
-  (** {3 Main API *)
-
-  val assert_eq : t -> term -> term -> Expl.t -> unit
-  (** Assert that two terms are equal, using the given explanation. *)
-
-  val assert_lit : t -> lit -> unit
-  (** Given a literal, assume it in the congruence closure and propagate
-      its consequences. Will be backtracked.
-
-      Useful for the theory combination or the SAT solver's functor *)
-
-  val assert_lits : t -> lit Iter.t -> unit
-  (** Addition of many literals *)
-
-  val check : t -> Result_action.or_conflict
-  (** Perform all pending operations done via {!assert_eq}, {!assert_lit}, etc.
-      Will use the {!actions} to propagate literals, declare conflicts, etc. *)
-
-  val push_level : t -> unit
-  (** Push backtracking level *)
-
-  val pop_levels : t -> int -> unit
-  (** Restore to state [n] calls to [push_level] earlier. Used during backtracking. *)
-
-  val get_model : t -> E_node.t Iter.t Iter.t
-  (** get all the equivalence classes so they can be merged in the model *)
-end
-
-(* TODO
-   module type DYN_BUILDER = sig
-     include ARGS_CLASSES_EXPL_EVENT
-   end
-*)
-
-(* TODO: full EGG, also have a function to update the value when
-   the subterms (produced in [of_term]) are updated *)
-
-(** Data attached to the congruence closure classes.
-
-    This helps theories keeping track of some state for each class.
-    The state of a class is the monoidal combination of the state for each
-    term in the class (for example, the set of terms in the
-    class whose head symbol is a datatype constructor). *)
-module type MONOID_PLUGIN_ARG = sig
-  module CC : S
-
-  type t
-  (** Some type with a monoid structure *)
-
-  include Sidekick_sigs.PRINT with type t := t
-
-  val name : string
-  (** name of the monoid structure (short) *)
-
-  (* FIXME: for subs, return list of e_nodes, and assume of_term already
-     returned data for them. *)
-  val of_term :
-    CC.t -> CC.E_node.t -> CC.term -> t option * (CC.E_node.t * t) list
-  (** [of_term n t], where [t] is the term annotating node [n],
-      must return [maybe_m, l], where:
-
-      - [maybe_m = Some m] if [t] has monoid value [m];
-        otherwise [maybe_m=None]
-      - [l] is a list of [(u, m_u)] where each [u]'s term
-        is a direct subterm of [t]
-        and [m_u] is the monoid value attached to [u].
-
-      *)
-
-  val merge :
-    CC.t ->
-    CC.E_node.t ->
-    t ->
-    CC.E_node.t ->
-    t ->
-    CC.Expl.t ->
-    (t * CC.Handler_action.t list, CC.Handler_action.conflict) result
-  (** Monoidal combination of two values.
-
-      [merge cc n1 mon1 n2 mon2 expl] returns the result of merging
-      monoid values [mon1] (for class [n1]) and [mon2] (for class [n2])
-      when [n1] and [n2] are merged with explanation [expl].
-
-      @return [Ok mon] if the merge is acceptable, annotating the class of [n1 ∪ n2];
-      or [Error expl'] if the merge is unsatisfiable. [expl'] can then be
-      used to trigger a conflict and undo the merge.
-    *)
-end
-
-(** Stateful plugin holding a per-equivalence-class monoid.
-
-    Helps keep track of monoid state per equivalence class.
-    A theory might use one or more instance(s) of this to
-    aggregate some theory-specific state over all terms, with
-    the information of what terms are already known to be equal
-    potentially saving work for the theory. *)
-module type DYN_MONOID_PLUGIN = sig
-  module M : MONOID_PLUGIN_ARG
-  include Sidekick_sigs.DYN_BACKTRACKABLE
-
-  val pp : unit Fmt.printer
-
-  val mem : M.CC.E_node.t -> bool
-  (** Does the CC E_node.t have a monoid value? *)
-
-  val get : M.CC.E_node.t -> M.t option
-  (** Get monoid value for this CC E_node.t, if any *)
-
-  val iter_all : (M.CC.repr * M.t) Iter.t
-end
-
-(** Builder for a plugin.
-
-    The builder takes a congruence closure, and instantiate the
-    plugin on it. *)
-module type MONOID_PLUGIN_BUILDER = sig
-  module M : MONOID_PLUGIN_ARG
-
-  module type DYN_PL_FOR_M = DYN_MONOID_PLUGIN with module M = M
-
-  type t = (module DYN_PL_FOR_M)
-
-  val create_and_setup : ?size:int -> M.CC.t -> t
-  (** Create a new monoid state *)
-end
diff --git a/src/sigs/cc/view.ml b/src/sigs/cc/view.ml
deleted file mode 100644
index e319f5ef..00000000
--- a/src/sigs/cc/view.ml
+++ /dev/null
@@ -1,38 +0,0 @@
-type ('f, 't, 'ts) t =
-  | Bool of bool
-  | App_fun of 'f * 'ts
-  | App_ho of 't * 't
-  | If of 't * 't * 't
-  | Eq of 't * 't
-  | Not of 't
-  | Opaque of 't
-(* do not enter *)
-
-let map_view ~f_f ~f_t ~f_ts (v : _ t) : _ t =
-  match v with
-  | Bool b -> Bool b
-  | App_fun (f, args) -> App_fun (f_f f, f_ts args)
-  | App_ho (f, a) -> App_ho (f_t f, f_t a)
-  | Not t -> Not (f_t t)
-  | If (a, b, c) -> If (f_t a, f_t b, f_t c)
-  | Eq (a, b) -> Eq (f_t a, f_t b)
-  | Opaque t -> Opaque (f_t t)
-
-let iter_view ~f_f ~f_t ~f_ts (v : _ t) : unit =
-  match v with
-  | Bool _ -> ()
-  | App_fun (f, args) ->
-    f_f f;
-    f_ts args
-  | App_ho (f, a) ->
-    f_t f;
-    f_t a
-  | Not t -> f_t t
-  | If (a, b, c) ->
-    f_t a;
-    f_t b;
-    f_t c
-  | Eq (a, b) ->
-    f_t a;
-    f_t b
-  | Opaque t -> f_t t
diff --git a/src/sigs/cc/view.mli b/src/sigs/cc/view.mli
deleted file mode 100644
index 038ea1a6..00000000
--- a/src/sigs/cc/view.mli
+++ /dev/null
@@ -1,33 +0,0 @@
-(** View terms through the lens of the Congruence Closure *)
-
-(** A view of a term fron the point of view of the congruence closure.
-
-      - ['f] is the type of function symbols
-      - ['t] is the type of terms
-      - ['ts] is the type of sequences of terms (arguments of function application)
-  *)
-type ('f, 't, 'ts) t =
-  | Bool of bool
-  | App_fun of 'f * 'ts
-  | App_ho of 't * 't
-  | If of 't * 't * 't
-  | Eq of 't * 't
-  | Not of 't
-  | Opaque of 't  (** do not enter *)
-
-val map_view :
-  f_f:('a -> 'b) ->
-  f_t:('c -> 'd) ->
-  f_ts:('e -> 'f) ->
-  ('a, 'c, 'e) t ->
-  ('b, 'd, 'f) t
-(** Map function over a view, one level deep.
-    Each function maps over a different type, e.g. [f_t] maps over terms *)
-
-val iter_view :
-  f_f:('a -> unit) ->
-  f_t:('b -> unit) ->
-  f_ts:('c -> unit) ->
-  ('a, 'b, 'c) t ->
-  unit
-(** Iterate over a view, one level deep. *)
diff --git a/src/sigs/lit/dune b/src/sigs/lit/dune
deleted file mode 100644
index 3774c2ba..00000000
--- a/src/sigs/lit/dune
+++ /dev/null
@@ -1,5 +0,0 @@
-(library
- (name sidekick_sigs_lit)
- (public_name sidekick.sigs.lit)
- (synopsis "Common definition for literals")
- (libraries containers iter sidekick.sigs sidekick.sigs.term))
diff --git a/src/sigs/lit/sidekick_sigs_lit.ml b/src/sigs/lit/sidekick_sigs_lit.ml
deleted file mode 100644
index 4acc4277..00000000
--- a/src/sigs/lit/sidekick_sigs_lit.ml
+++ /dev/null
@@ -1,45 +0,0 @@
-(** Literals
-
-    Literals are a pair of a boolean-sorted term, and a sign.
-    Positive literals are the same as their term, and negative literals
-    are the negation of their term.
-
-    The SAT solver deals only in literals and clauses (sets of literals).
-    Everything else belongs in the SMT solver. *)
-
-module type TERM = Sidekick_sigs_term.S
-
-module type S = sig
-  module T : TERM
-  (** Literals depend on terms *)
-
-  type t
-  (** A literal *)
-
-  include Sidekick_sigs.EQ_HASH_PRINT with type t := t
-
-  val term : t -> T.Term.t
-  (** Get the (positive) term *)
-
-  val sign : t -> bool
-  (** Get the sign. A negated literal has sign [false]. *)
-
-  val neg : t -> t
-  (** Take negation of literal. [sign (neg lit) = not (sign lit)]. *)
-
-  val abs : t -> t
-  (** [abs lit] is like [lit] but always positive, i.e. [sign (abs lit) = true] *)
-
-  val signed_term : t -> T.Term.t * bool
-  (** Return the atom and the sign *)
-
-  val atom : ?sign:bool -> T.Term.store -> T.Term.t -> t
-  (** [atom store t] makes a literal out of a term, possibly normalizing
-      its sign in the process.
-      @param sign if provided, and [sign=false], negate the resulting lit. *)
-
-  val norm_sign : t -> t * bool
-  (** [norm_sign (+t)] is [+t, true],
-      and [norm_sign (-t)] is [+t, false].
-      In both cases the term is positive, and the boolean reflects the initial sign. *)
-end
diff --git a/src/sigs/proof-core/dune b/src/sigs/proof-core/dune
deleted file mode 100644
index 8eb404e9..00000000
--- a/src/sigs/proof-core/dune
+++ /dev/null
@@ -1,6 +0,0 @@
-(library
- (name sidekick_sigs_proof_core)
- (public_name sidekick.sigs.proof.core)
- (synopsis "Common rules for proof traces")
- (flags :standard -open Sidekick_util)
- (libraries containers iter sidekick.util sidekick.sigs))
diff --git a/src/sigs/proof-core/sidekick_sigs_proof_core.ml b/src/sigs/proof-core/sidekick_sigs_proof_core.ml
deleted file mode 100644
index 7bc87bb2..00000000
--- a/src/sigs/proof-core/sidekick_sigs_proof_core.ml
+++ /dev/null
@@ -1,94 +0,0 @@
-(** Proof rules for common operations and congruence closure *)
-
-module type S = sig
-  type rule
-  type term
-  type lit
-
-  type step_id
-  (** Identifier for a proof proof_rule (like a unique ID for a clause previously
-      added/proved) *)
-
-  val lemma_cc : lit Iter.t -> rule
-  (** [lemma_cc proof lits] asserts that [lits] form a tautology for the theory
-      of uninterpreted functions. *)
-
-  val define_term : term -> term -> rule
-  (** [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 : step_id -> step_id -> rule
-  (** [proof_p1 p1 p2], where [p1] proves the unit clause [t=u] (t:bool)
-      and [p2] proves [C \/ t], is the rule that produces [C \/ u],
-      i.e unit paramodulation. *)
-
-  val proof_r1 : step_id -> step_id -> rule
-  (** [proof_r1 p1 p2], where [p1] proves the unit clause [|- t] (t:bool)
-      and [p2] proves [C \/ ¬t], is the rule that produces [C \/ u],
-      i.e unit resolution. *)
-
-  val proof_res : pivot:term -> step_id -> step_id -> rule
-  (** [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 rule that produces [C \/ D], i.e boolean resolution. *)
-
-  val with_defs : step_id -> step_id Iter.t -> rule
-  (** [with_defs pr defs] specifies that [pr] is valid only in
-      a context where the definitions [defs] are present. *)
-
-  val lemma_true : term -> rule
-  (** [lemma_true (true) p] asserts the clause [(true)] *)
-
-  val lemma_preprocess : term -> term -> using:step_id Iter.t -> rule
-  (** [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 rule ID for the clause [(t=u)]. *)
-
-  val lemma_rw_clause :
-    step_id -> res:lit Iter.t -> using:step_id Iter.t -> rule
-  (** [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). *)
-end
-
-type ('rule, 'step_id, 'term, 'lit) t =
-  (module S
-     with type rule = 'rule
-      and type step_id = 'step_id
-      and type term = 'term
-      and type lit = 'lit)
-
-(** Make a dummy proof with given types *)
-module Dummy (A : sig
-  type rule
-  type step_id
-  type term
-  type lit
-
-  val dummy_rule : rule
-end) :
-  S
-    with type rule = A.rule
-     and type step_id = A.step_id
-     and type term = A.term
-     and type lit = A.lit = struct
-  include A
-
-  let lemma_cc _ = dummy_rule
-  let define_term _ _ = dummy_rule
-  let proof_p1 _ _ = dummy_rule
-  let proof_r1 _ _ = dummy_rule
-  let proof_res ~pivot:_ _ _ = dummy_rule
-  let with_defs _ _ = dummy_rule
-  let lemma_true _ = dummy_rule
-  let lemma_preprocess _ _ ~using:_ = dummy_rule
-  let lemma_rw_clause _ ~res:_ ~using:_ = dummy_rule
-end
diff --git a/src/sigs/proof-sat/dune b/src/sigs/proof-sat/dune
deleted file mode 100644
index baa7cc5f..00000000
--- a/src/sigs/proof-sat/dune
+++ /dev/null
@@ -1,6 +0,0 @@
-(library
- (name sidekick_sigs_proof_sat)
- (public_name sidekick.sigs.proof.sat)
- (synopsis "SAT-solving rules for proof traces")
- (flags :standard -open Sidekick_util)
- (libraries containers iter sidekick.util sidekick.sigs))
diff --git a/src/sigs/proof-sat/sidekick_sigs_proof_sat.ml b/src/sigs/proof-sat/sidekick_sigs_proof_sat.ml
deleted file mode 100644
index c9b20417..00000000
--- a/src/sigs/proof-sat/sidekick_sigs_proof_sat.ml
+++ /dev/null
@@ -1,22 +0,0 @@
-(** Proof rules for SAT Solver reasoning *)
-
-module type S = sig
-  type rule
-  (** The stored proof (possibly nil, possibly on disk, possibly in memory) *)
-
-  type step_id
-  (** identifier for a proof *)
-
-  type lit
-  (** A boolean literal for the proof trace *)
-
-  val sat_input_clause : lit Iter.t -> rule
-  (** Emit an input clause. *)
-
-  val sat_redundant_clause : lit Iter.t -> hyps:step_id Iter.t -> rule
-  (** Emit a clause deduced by the SAT solver, redundant wrt previous clauses.
-      The clause must be RUP wrt [hyps]. *)
-
-  val sat_unsat_core : lit Iter.t -> rule
-  (** TODO: is this relevant here? *)
-end
diff --git a/src/sigs/proof-trace/dune b/src/sigs/proof-trace/dune
deleted file mode 100644
index 19c97cd6..00000000
--- a/src/sigs/proof-trace/dune
+++ /dev/null
@@ -1,5 +0,0 @@
-(library
- (name sidekick_sigs_proof_trace)
- (public_name sidekick.sigs.proof-trace)
- (synopsis "Common definition for proof traces")
- (libraries containers iter sidekick.sigs sidekick.util))
diff --git a/src/sigs/proof-trace/sidekick_sigs_proof_trace.ml b/src/sigs/proof-trace/sidekick_sigs_proof_trace.ml
deleted file mode 100644
index 83ee8d3f..00000000
--- a/src/sigs/proof-trace/sidekick_sigs_proof_trace.ml
+++ /dev/null
@@ -1,42 +0,0 @@
-(** Proof traces.
-*)
-
-open Sidekick_util
-
-module type ARG = sig
-  type rule
-
-  type 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. *)
-end
-
-module type S = sig
-  module A : ARG
-
-  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 -> A.rule -> A.step_id
-  (** Create a new step in the trace. *)
-
-  val add_unsat : t -> A.step_id -> unit
-  (** Signal "unsat" result at the given proof *)
-
-  val delete : t -> A.step_id -> unit
-  (** Forget a step that won't be used in the rest of the trace.
-      Only useful for performance/memory considerations. *)
-end
diff --git a/src/sigs/term/dune b/src/sigs/term/dune
deleted file mode 100644
index 3c461792..00000000
--- a/src/sigs/term/dune
+++ /dev/null
@@ -1,5 +0,0 @@
-(library
- (name sidekick_sigs_term)
- (public_name sidekick.sigs.term)
- (synopsis "Common definition for terms and types")
- (libraries containers iter sidekick.sigs))
diff --git a/src/sigs/term/sidekick_sigs_term.ml b/src/sigs/term/sidekick_sigs_term.ml
deleted file mode 100644
index bf82f0c7..00000000
--- a/src/sigs/term/sidekick_sigs_term.ml
+++ /dev/null
@@ -1,80 +0,0 @@
-(** Main representation of Terms and Types *)
-module type S = sig
-  module Fun : Sidekick_sigs.EQ_HASH_PRINT
-  (** A function symbol, like "f" or "plus" or "is_human" or "socrates" *)
-
-  (** Types
-
-      Types should be comparable (ideally, in O(1)), and have
-      at least a boolean type available. *)
-  module Ty : sig
-    include Sidekick_sigs.EQ_HASH_PRINT
-
-    type store
-
-    val bool : store -> t
-    val is_bool : t -> bool
-  end
-
-  (** Term structure.
-
-      Terms should be {b hashconsed}, with perfect sharing.
-      This allows, for example, {!Term.Tbl} and {!Term.iter_dag} to be efficient.
-  *)
-  module Term : sig
-    include Sidekick_sigs.EQ_ORD_HASH_PRINT
-
-    type store
-    (** A store used to create new terms. It is where the hashconsing
-        table should live, along with other all-terms related store. *)
-
-    val ty : t -> Ty.t
-
-    val bool : store -> bool -> t
-    (** build true/false *)
-
-    val as_bool : t -> bool option
-    (** [as_bool t] is [Some true] if [t] is the term [true], and similarly
-        for [false]. For other terms it is [None]. *)
-
-    val abs : store -> t -> t * bool
-    (** [abs t] returns an "absolute value" for the term, along with the
-        sign of [t].
-
-        The idea is that we want to turn [not a] into [(a, false)],
-        or [(a != b)] into [(a=b, false)]. For terms without a negation this
-        should return [(t, true)].
-
-        The store is passed in case a new term needs to be created. *)
-
-    val map_shallow : store -> (t -> t) -> t -> t
-    (** Map function on immediate subterms. This should not be recursive. *)
-
-    val iter_shallow : store -> (t -> unit) -> t -> unit
-    (** Iterate function on immediate subterms. This should not be recursive. *)
-
-    val iter_dag : t -> (t -> unit) -> unit
-    (** [iter_dag t f] calls [f] once on each subterm of [t], [t] included.
-        It must {b not} traverse [t] as a tree, but rather as a
-        perfectly shared DAG.
-
-        For example, in:
-        {[
-          let x = 2 in
-          let y = f x x in
-          let z = g y x in
-          z = z
-        ]}
-
-        the DAG has the following nodes:
-
-        {[ n1: 2
-           n2: f n1 n1
-           n3: g n2 n1
-           n4: = n3 n3
-         ]}
-    *)
-
-    module Tbl : CCHashtbl.S with type key = t
-  end
-end